http://gcc.gnu.org/bugzilla/show_bug.cgi?id=50642
Manuel López-Ibáñez <manu at gcc dot gnu.org> changed: What |Removed |Added ---------------------------------------------------------------------------- CC| |manu at gcc dot gnu.org --- Comment #8 from Manuel López-Ibáñez <manu at gcc dot gnu.org> 2013-04-18 10:02:13 UTC --- (In reply to comment #7) > > Please change the font size to normal. If it appears similar to the text, a > different font family can be used. Please send a patch to gcc-patches with [wwwdocs] in the subsject. My guess is that nobody cares enough to bother to submit a patch. If someone submitted a patch, Gerald most likely will approve it.