changeset 53715 | 68c664737d04 |
parent 53639 | 09a4954e7c07 |
child 53884 | 48d13465c7c7 |
--- a/src/Tools/jEdit/etc/options Wed Sep 18 16:18:17 2013 +0200 +++ b/src/Tools/jEdit/etc/options Wed Sep 18 20:09:26 2013 +0200 @@ -3,6 +3,9 @@ public option jedit_logic : string = "" -- "default logic session" +public option jedit_auto_load : bool = false + -- "load all required files automatically to resolve theory imports" + public option jedit_reset_font_size : int = 18 -- "reset font size for main text area"