This is the result of some bug-hunting. But I don't know if it makes any
difference. It isn't worse, at least.