Effectively revert the previous change: leave the new #include in, but

comment it out with an explanation.  This makes it easier for someone
who wants the additional symbols to try re-enabling it for their platform.