a1e12d602d
It was added in 6ff1a1f8a6, but we never really needed
it since then.
Since MS is currently down and this causes CI to fail, it's a good time
to remove it.
If we need it again it's always in the git history..
a1e12d602d