Reduced header font sizes, and upped the size of monospace font in
diffs. Should be better in Windows now. Closes #248.
Authored by: daniel 2004-05-13
Parent: [r507]
Child: [r509]
