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?
