Cannot change font size of built-in terminal
I did not find a way to change the font size of the terminal plugin.
I went to dconf-editor, and changed org.gnome.gedit.plugins.terminal.font and org.gnome.gedit.plugins.terminal.use-system-font, but it had no effect.
Did I miss something?
Edited by Frédéric Parrenin