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.
1 file changed