---- On Wed, 12 Feb 2020 23:26:22 -0500 Gábor Boskovits <boskov...@gmail.com> wrote ---- > Hello, > > Christopher Baines <m...@cbaines.net> ezt írta (időpont: 2020. febr. 13., > Csü 0:55): > > > > > Ludovic Courtès <l...@gnu.org> writes: > > > > > Hello! > > > > > > sirgazil <sirga...@zoho.com> skribis: > > > > > >> I have GNOME 3.32.2 now. When I launched a GNOME Terminal, I noticed > > that the font is too big and the spacing between characters seems odd: > > >> > > >> > > https://multimedialib.files.wordpress.com/2020/01/terminal-font-problem-2020-01-08.png > > >> > > >> Maybe there is a bug with the defaults (at least with the spacing)? > > > > > > This problem still shows up in ‘guix system vm’, so it’s not related to > > > state. > > > > > > Any idea how to fix it? > > > > I think I encountered this, I "fixed" it by going in to the Tweaks app > > and selecting some fonts where previously I think some options didn't > > have a font selected. > > > Same thing here. It would be nice if we could somehow manipulate these > setting from a script/dotfile, but I did not go deep into finding out how > that work. Anyone has any idea if that is supported?
But whose setting is not properly set? GNOME Terminal, GNOME, ...? :) As far as I understand, GNOME applications use GSettings for application settings and gschema XML files (https://developer.gnome.org/gio/stable/GSettings.html). GNOME Terminal, for example, comes with a gschema XML file which defines default values: https://gitlab.gnome.org/GNOME/gnome-terminal/blob/gnome-3-32/src/org.gnome.Terminal.gschema.xml By default, the application seems to be set to use the system monospace font. So why is it that the font value in the default GNOME Terminal profile is not set. I don't remember if it appears empty or set to "None 10".
