Changing fonts

2000-06-04 Thread Frédéric Delacroix
Hello, I'm using texinfo 2.222 and I'm looking for a way to make it use smaller fonts (my manual is 135 pages and I want it smaller). I'd like to use eight point fonts for the main text. I didn't see in the docs a way to do this at the document level, and I'm confused when looking at

Re: Changing fonts

2000-06-04 Thread Karl Berry
eight point fonts for the main text. To do this, you need to hack texinfo.tex. I can't give you an exact recipe, but the fonts are defined at the 50 lines or so starting at \ifx\bigger\relax \let\mainmagstep=\magstep1 \setfont\textrm\rmshape{12}{1000}