On Fri, Jul 17, 2026 at 09:41:45AM +0000, Dimitris Papavasiliou wrote: > Please see comments below. > > On Thursday, July 16th, 2026 at 5:47 PM, Gavin Smith > <[email protected]> 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. > > > > 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]> > > > 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. > > > > 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? >
I am not an expert on LaTeX. My go-to resource is "An unofficial reference manual" (https://latexref.xyz/). The following page suggests you can use a "12pt" option in a "document size option": https://latexref.xyz/Font-sizes.html "LaTeX - A Document Preparation System" (Leslie Lamport, 1994) is the closest document I know of to an "official" manual for LaTeX, although would be slightly dated, I expect.
