Karl: The same problem was also reported as bug 65730, with a patch
Thanks Zack. I had just composed a reply saying just about exactly the
same thing as you wrote :).
I will merge the patches and try Bogdan's test, no problem. -k
P.S. Bogdan, sorry that I wasn't thinking more clearly when I
> Karl Berry , Fri Sep 01 2023 00:28:04 GMT+0200
> (Central European Summer Time)
>> Bogdan: I will adjust the patch, one way or another. Nothing more for
>> you to do here after all :). --thanks, karl.
Karl: The same problem was also reported as bug 65730, with a patch
supplied by Łukasz Stelmach
