On Tue, Nov 17, 2020 at 08:13:29AM +0100, Werner LEMBERG wrote: > Irrespective of that I wonder what must be done in the future to make > `@smallexample` be output with smaller type in HTML...
It's probably not possible. You could make both @example and @smallexample smaller everywhere using CSS. I don't know any way of applying CSS rules to just a part of the manual. There are other possibilities like directly writing something like @html <pre class='small'> .... </pre> @end html plus CSS rules. This is complicated but hopefully not necessary in too many places.
