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? Best regards, g_bor >
