This was overlooked in r80804.  This change is not really a bug fix,
but the release manager agreed to it.  There is no NEWS entry, like
in the original commit.