# HG changeset patch
# User wenzelm
# Date 1439991659 -7200
# Node ID d94f3afd69b6dcead0fd6bf11f99f79234ac8a97
# Parent  4fc4681970407d2f1509d905cf8e7b572d956e69
disabled auto resolve, until practical consequences are more clear;

diff -r 4fc468197040 -r d94f3afd69b6 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Aug 18 17:06:34 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Aug 19 15:40:59 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