This reverts commit 7e6c518ce4.
I misinterpreted Github's CI failure in the notification tab and
thought that I had broken CI on origin/master, so I panic-reverted
before I merged it (I thought they had).
On closer inspection, it appears that the CI failure was not from
the tip that I merged. This PR resubmits the reverted change. I'll
wait for OfBorg to finish this time.