[Bug web/50642] onlinedocs formated text too small to read

[jg at jguk dot org]

http://gcc.gnu.org/bugzilla/show_bug.cgi?id=50642

--- Comment #6 from Jon Grant <jg at jguk dot org> 2011-11-12 22:15:36 UTC ---
Could this be followed up with the proposed change implemented?

pre.smallexample { font-size:normal }

Thanks, Jon