@Max who is handling this fix is on PTO for a week and I'm not aware of the state of the second PR. But your comment is correct, the first PR is already merged. We can look into cutting a new release soon.