Manually reverting the change from #999, because it breaks.

Fixes #1007. That is to say: it doesn’t break anymore, and I’ve written
a short comment about why it doesn’t work.