This reverts commit c6d26b7f. The hack isn't needed anymore. No change in output compared to the parent commit (except for hashes).