Re: rethinking @def*

[pertusus]

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