Hello,

I found out there is a "DPI" setting in Gnome. The default setting is not always the same. You can find the setting here:

system | preferences | appearance | fonts | button "details" (rough translated from Dutch in English)

Not sure this solves the problem completely.

With regards, Paul van der Vlis.

-- http://www.vandervlis.nl/