Committed as 9c2b1d37e729f7af9e9661be7ece8348bae70ffa

I think the bug can be closed, but I don't see how I could do that.  Or maybe I can't and shouldn't, I don't know.