and another thing

I finally found the “other bug”: today, and more or less fixed it. Nobody in particular will care, I’m sure. (I say “more or less” because I’m not sure if people are going to go for my solution. I’m ready to wash my hands of it, though.)

Comments are closed.