All of the GUI strings and text are now formatted with a small sans serif font in the user manual.
This is because in the GUI, a sans serif font is almost always used be default.
Authored by: bugman 2012-09-19
Parent: [r17505]
Child: [r17507]
