05dddb71b0
This reverts commit 9cce18a585.
rB9cce18a5858c broke the build in unforeseen ways, not easily fixable.
revert for now, so master will at least build again.