> This fix seems uncontroversial, so I have merged it; thank you. I've
> never run into this problem myself; do you remember how you triggered
> it?
Sorry, I don't remember. It's been quite some time...
Juliusz