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.
