Since I'm overdue for another browser question...
It seems easy enough to change fonts in links; however,
Font13, which seems to be the font for most text, is,
by default, associated with lucidasans/unicode.7.font,
which is a bit small. When I change `7' to `8' though,
there is no corresponding change in leading, so I get
tightly packed lines and truncated descenders.
How do I do this right?