Revert PR
#5388
We realised that
#5388 introduces a different problem of about the same
magnitude as the one it fixes (both are quite minor). A proper fix would
be too invasive this close to release, and after discussion, we decided
it was better to leave the same problem that has been in previous
releases.