src/Tools/jEdit/etc/options
changeset 60916 a6e2a667b0a8
parent 60914 f39d004f2ff4
child 60973 d94f3afd69b6
--- a/src/Tools/jEdit/etc/options	Wed Aug 12 03:07:01 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Aug 12 13:53:51 2015 +0200
@@ -9,6 +9,9 @@
 public option jedit_auto_load : bool = false
   -- "load all required files automatically to resolve theory imports"
 
+public option jedit_auto_resolve : bool = true
+  -- "automatically resolve auxiliary files within the editor"
+
 public option jedit_reset_font_size : int = 18
   -- "reset main text font size"