Does @smallexample come out as 8pt or so? It definitely looks
smaller than 10pt on my screen.
It comes out as whatever your browser tells it to, hopefully depending
on what font size you have set. This is why different users see
different things. The effect should be similar to using
<small>...</small>, although I expect there are browser(s) and
version(s) which don't implement any of this properly in the first
place.
As for using @example instead of @smallexample, I suspect some of the
examples would then become too wide for the printed manual.
I'm sorry, but I just don't see anything to do here. Every option will
displease someone.
karl
