Mario Pietsch cee7baa183 Make editor font configurable, so user can easily change it to eg monospace font (#2867)		2017-06-29 16:55:49 +01:00
..
base.tid	Make editor font configurable, so user can easily change it to eg monospace font (#2867)	2017-06-29 16:55:49 +01:00
plugin.info	Consistent plugin descriptions	2015-02-17 10:28:54 +00:00