Re: Vertical spacing between @deffn output and preceding text

On Fri, Jul 17, 2026 at 09:41:45AM +0000, Dimitris Papavasiliou wrote:
> Since we're on the subject, how would I
> best go about changing the font size in Latex to 12pt?  The
> `@fontsize` command only supports 10 or 11pt.  I've added
> 
> \usepackage{fontsize}
> \changefontsize{12}
> 
> to my LaTex preamble, which seems to get the job done, but perhaps
> there's a more appropriate way to do it?

That's the LaTeX code used for other values of @fonttextsize, so if it
is not appropriate, we would need to change that...

-- 
Pat