Я использую расширение панели и хочу изменить шрифт по умолчанию. Поэтому я изменил gnome-shell.css в / usr / share / themes / theme_name /. Я написал новую строку (font-family) в разделе / Top Bar /.
/* Top Bar */
#panel {
font-family: Ubuntu Bold;
background-color: #1d1d1d;
height: 1.86em;
font-feature-settings: "tnum"; }
(...)
Я хочу использовать шрифт Ubuntu BOLD (!). Кажется, что gnome меняет шрифт, но это просто Ubuntu Regular (он тонкий), и я понятия не имею, как мне использовать Ubuntu Bold.
Семейства шрифтов Ubuntu Bold не существует. Это не проверено, но я бы попробовал:
font-family: Ubuntu;
font-weight: bold;
Редактировать:
Я создал эту тестовую страницу. Проверьте источник этой страницы.
Таким образом, указание шрифта каким-то образом должно быть тем, что необходимо.