Ah stupid. It appears that @mart pushed the same fix as part of commit 63a7f75a79c1685268. So this one can be reverted. Sorry. Well, that happens when stuff is sitting around for 6 weeks.

Ok, accepted within 7 minutes after creation, but not merged since then (19 november). Do I need to do something? Maybe I just do not understand the development model, merge rights etc?

No commit access for me. Not needed, as I do not expect a huge amount of work on the repo. It is perfectly fine when mart commits it.