src/Tools/jEdit/etc/options
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"