Probably a very basic question, bu how to change the font size of the
dvi output?Unfortunately, there is no easy way to change the font sizes. I can't come up with a recipe off the top of my head, except to change the numbers in texinfo.tex. Maybe someone else on the list has tackled this ... _______________________________________________ Texinfo home page: http://www.gnu.org/software/texinfo [email protected] http://lists.gnu.org/mailman/listinfo/help-texinfo
