Re: rethinking @def*

[Gavin Smith]

On Sun, Jul 31, 2022 at 07:46:02PM +0200, pertusus@free.fr wrote:
> In HTML, with firefox, the typewriter face is smaller than the other
> faces which is suboptimal for the @def* formatting, and probably all
> over documents.  But I think that we should not do anything and leave
> that to the browser.

I'd never noticed that before, but you are right, it is like that
everywhere (in Chromium too).  I think we should just accept it.