Re: Vertical spacing between @deffn output and preceding text

Please see comments below.

On Thursday, July 16th, 2026 at 5:47 PM, Gavin Smith <gavinsmith0123@gmail.=
com> wrote:

> On Thu, Jul 16, 2026 at 12:20:18PM +0000, Dimitris Papavasiliou wrote:
> > Thanks for looking into this so quickly!  Please let me know if you
> > merge this to master, or some other branch, so that I can try to build
> > it and try it out.
>=20
> Committed today, in git commit 83e09236dd.

I've compiled and tried it out.  The result looks fine!

> > On Thursday, July 16th, 2026 at 1:26 PM, Patrice Dumas <[email protected]=
r> wrote:

> No.  The point of the LaTeX output is to produce output in a plain,
> unsurprising, idiomatic LaTeX style.  This is to make it easier for
> users to undersand the output and customise it to their needs using
> various LaTeX features and packages.
>=20
> In other terms, the LaTeX output file is an end in itself, and not
> merely an intermediate step for creating a PDF.

I see.  This makes sense.  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?