Daniel-Constantin Mierla writes:

> I think this was fixed by commit
> 4994960324d5353222b3de08515bed07802ab7bc, if not, reopen.

Yes, I didn't remember that I had opened an issue about it.

-- Juha


You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or mute the thread.