@jdemeyer Could you apply the suggested change so we can merge? Or else select the "Allow edits from maintainers" checkbox on the right hand side and let us know so we can finish it off.

Or else select the "Allow edits from maintainers" checkbox on the right hand side

It was already checked :-)

@zooba:

Or else select the "Allow edits from maintainers" checkbox on the right hand side and let us know so we can finish it off.

As far as I'm aware, that option is supposed to allow anyone with write access to the repository to directly commit suggestions to the PR branch. But, it doesn't always work correctly in my experience. The GitHub interface may not be recognizing that I made an actual suggestion, since I chose "Approve" when I added my review instead of "Request changes" or "Comment".

I'll try to do it again, but instead select the "Request changes" option this time.

No, the original submitter has to select the checkbox on the right to allow maintainers to push changes to their branch. We think it changed from default-checked to default-unchecked at some point.

I'll just merge this and then apply your suggestion myself.

Oh, just spotted Jeroen's comment in amongst all the rest of the boxes here (still not a fan of this UI...). Weird that it wasn't working, but it's done now so 🤷‍♂️