The font size is no longer set for the latex2html compiled user manual.
Authored by: bugman 2013-08-07
Parent: [r20565]
Child: [r20567]
