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
