Re: [help-texinfo] changing font size in hardcopy

[Karl Berry]

    Is there a reason why `\magnification' wouldn't work?  

It'll reset the page size to plain.tex's defaults.  But Matthias, you
could try this (near the beginning of the doc):

@tex
\globaldefs=1
\magnification=1200
@end tex

If the result looks approximately usable, I could think about another
version that keeps Texinfo's sizes.

Thanks Laurence.