more thorough reload;
authorwenzelm
Wed, 12 Aug 2015 13:56:46 +0200
changeset 60917 0607869c2ff3
parent 60916 a6e2a667b0a8
child 60918 4ceef1592e8c
child 60923 020becec359c
more thorough reload;
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()
   }