9a386574d8
This reverts commit 208feceb03.
Changes requested in the PR not made. Such a change requires
discussion on the list first.