Рабочее окружение Mate.
Итак, как оказалось, что-то все-таки можно сделать. Открываем терминал и пишем волшебное:
Код PHP:
Далее ищем две строчки со словами font_name и меняем значение в кавычках на необходимое (то есть, к примеру, "9" меняем на "12"). Данный способ работает для темы по умолчанию. Я так понял, можно (и даже больше того - нужно!) поменять не только размер шрифта, но и семейство. То есть пишем, к примеру, "Ubuntu, 11" для font_name.
sudo gvim /usr/share/themes/Mint-X-Metal/gtk-2.0/gtkrc
После нескольких перезагрузок, я остановил свой выбор на таком варианте: "FreeSans, 11".