This reverts commit 99d912d3. Looks like Johan managed to botch a merge somehow, see #1786. Or maybe that was a bug on the GitHub side. (cherry picked from commit d10d67cc)