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.