Jerry f5c14d2541 Add font size option, fixes #6		2022-06-07 18:51:11 +08:00
..
org.gnome.shell.extensions.activate_gnome.gschema.xml	Add font size option, fixes #6	2022-06-07 18:51:11 +08:00