# HG changeset patch
# User wenzelm
# Date 1439380606 -7200
# Node ID 0607869c2ff3b1ab92ef0a6a462ae436627664f3
# Parent  a6e2a667b0a84033683a95d0ac0e0d0e8dfae628
more thorough reload;

diff -r a6e2a667b0a8 -r 0607869c2ff3 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Aug 12 13:53:51 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Aug 12 13:56:46 2015 +0200
@@ -122,7 +122,7 @@
           if changed(model.node_name)
         } model.syntax_changed()
       }
-    if (PIDE.options.bool("jedit_auto_load") && change.deps_changed ||
+    if (change.deps_changed ||
         PIDE.options.bool("jedit_auto_resolve") && change.version.nodes.undefined_blobs.nonEmpty)
       PIDE.deps_changed()
   }