more thorough reload;
authorwenzelm
Wed Aug 12 13:56:46 2015 +0200 (2015-08-12 ago)
changeset 609170607869c2ff3
parent 60916 a6e2a667b0a8
child 60918 4ceef1592e8c
child 60923 020becec359c
more thorough reload;
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Aug 12 13:53:51 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Aug 12 13:56:46 2015 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4            if changed(model.node_name)
     1.5          } model.syntax_changed()
     1.6        }
     1.7 -    if (PIDE.options.bool("jedit_auto_load") && change.deps_changed ||
     1.8 +    if (change.deps_changed ||
     1.9          PIDE.options.bool("jedit_auto_resolve") && change.version.nodes.undefined_blobs.nonEmpty)
    1.10        PIDE.deps_changed()
    1.11    }