Sebastien, I rolled back the work-around above by using "--type int" and then updated, without success: the gnome-terminal still opens with tiny fonts. Applying the work-around again puts all gnome-terminal windows back to normal.
Sebastien, I rolled back the work-around above by using "--type int" and then updated, without success: the gnome-terminal still opens with tiny fonts. Applying the work-around again puts all gnome-terminal windows back to normal.