On Sunday, July 19th, 2026 at 3:01 PM, Gavin Smith <[email protected]>
wrote:
> As far as I can tell, Dimitris was successful in changing the font size,
> so there isn't a problem here to be solved by extending the @fontsize
> feature.
> It could be fine to edit the documentation if "@fonttextsize 12" actually
> works in LaTeX output.
It does not. It compains that "Only @fonttextsize 10 or 11 is
supported, not `12'". My solution works, so I aggree that nothing
needs to be fixed. My way of using Texinfo though, is by converting
text extracted from source comments or stand-alone documentation files
to Texino, so I need to assemble the final Texinfo source anyway and
adding the Latex commands is simple in this case. As far as I can
see, a more typical Texnifo user, would have to either figure out a
way to add the two lines
\usepackage{fontsize}
\changefontsize{12}
to the produced Latex output in a postprocessing step, or perhaps use
`@fonttextsize 11` in their Texinfo source and then replace the 11 in
`\changefontsize{11}` to 12, using sed. Both methods work fine now,
but are sensitive to the interal workings of Texinfo and the Latex
code it produces. Both are also rather awkward.
That wouldn't be a big issue if a special feature had to be
implemented to address this, but since `@fonttextsize` already exists,
not restricting the supported values might be a simple enough change
to warrant the effort.
