--- a/src/Tools/jEdit/src/jedit_resources.scala Wed Aug 12 03:07:01 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Aug 12 13:53:51 2015 +0200
@@ -122,6 +122,8 @@
if changed(model.node_name)
} model.syntax_changed()
}
- if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
+ if (PIDE.options.bool("jedit_auto_load") && change.deps_changed ||
+ PIDE.options.bool("jedit_auto_resolve") && change.version.nodes.undefined_blobs.nonEmpty)
+ PIDE.deps_changed()
}
}