Hi! Probably a very basic question, bu how to change the font size of the dvi output?
Regards Matthias _______________________________________________ Texinfo home page: http://www.gnu.org/software/texinfo [email protected] http://lists.gnu.org/mailman/listinfo/help-texinfo
