The following fixes it:
$ cd /etc/fonts/conf.d $ sudo rm 10-hinting-medium.conf $ sudo ln -s ../conf.avail/10-hinting-full.conf
So it seems that the configuration in /etc/fonts/conf.d overwrites the GNOME font preferences -- at least for GNOME Terminal.
The following fixes it:
$ cd /etc/fonts/conf.d medium. conf avail/10- hinting- full.conf
$ sudo rm 10-hinting-
$ sudo ln -s ../conf.
So it seems that the configuration in /etc/fonts/conf.d overwrites the GNOME font preferences -- at least for GNOME Terminal.