On Sun, Jul 31, 2022 at 02:38:17PM +0100, Gavin Smith wrote: > > I've got a different proposal now for the difference between > @deftypefn and @deffn (described above).
I tried to implement that proposal (at least what I had understood...) both in LaTeX and HTML. 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. -- Pat
