This reverts commit 15ee8a3a. It is a follow-up to b783f70a, which I'm reverting -- see the explanation in that revert.