disable jedit_auto_resolve (again) -- too confusing;
authorwenzelm
Tue, 08 Sep 2015 21:57:18 +0200
changeset 61139 f9fd43d8981d
parent 61138 dcbec1b22b07
child 61141 92858a52e45b
child 61142 6d29eb7c5fb2
disable jedit_auto_resolve (again) -- too confusing;
src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Sep 08 21:49:21 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 08 21:57:18 2015 +0200
@@ -9,7 +9,7 @@
 public option jedit_auto_load : bool = false
   -- "load all required files automatically to resolve theory imports"
 
-public option jedit_auto_resolve : bool = true
+public option jedit_auto_resolve : bool = false
   -- "automatically resolve auxiliary files within the editor"
 
 public option jedit_reset_font_size : int = 18