On Sun, Jul 31, 2022 at 07:46:02PM +0200, [email protected] 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.
