| changeset 53161 | 051cbf663b5f |
| parent 52874 | 91032244e4ca |
| child 53229 | 6ce8328d7912 |
--- a/src/Tools/jEdit/etc/options Fri Aug 23 11:23:26 2013 +0200 +++ b/src/Tools/jEdit/etc/options Fri Aug 23 11:41:17 2013 +0200 @@ -3,6 +3,9 @@ public option jedit_logic : string = "" -- "default logic session" +public option jedit_reset_font_size : int = 18 + -- "reset font size for main text area" + public option jedit_font_scale : real = 1.0 -- "scale factor of add-on panels wrt. main text area"