Hello Karl, Thanks for your reply. > >> I see in the HTML this is the code causing the small font: > >> > >> pre.smallexample { font-size:smaller } > > I don't know of any way to say "use a slightly smaller font" in > HTML/CSS. That is, this is what CSS provides, afaik. > > The reason that the above css exists at all is because users requested > that @smallexample (the Texinfo command in question) produce smaller > output than the regular @example, including in HTML. (Like > @smalldisplay, @smallformat, @smallisp, and now @smallquotation.) > Personally I don't have strong feelings about it.
Perhaps GCC could use @example rather than @smallexample ? Does @smallexample come out as 8pt or so? It definitely looks smaller than 10pt on my screen. Kind regards, Jon