Printing

[Lars Ræder <larsrc gmail com>]

[Writing from my gmail account, as my regular server is down until Friday]

In answer to Chris Green's post, I have observed some strange effects
with font sizes, too.  Occasionally, the font would get really huge or
very small.  Only under Windows have I noticed a difference in size
when printing, which is probably due to Windows printing using a
different API.
Definitely something that needs looking at, might well be the font
cache acting up somehow.

-Lars