Fix problems building documentation with newer versions of makeinfo.

Someone decided that makeinfo should parse commands inside
comments. This fix may seem incorrect, but it's the "official" one.
http://www.mail-archive.com/bug-binutils@gnu.org/msg14429.html