src/Tools/jEdit/src/jedit_resources.scala
changeset 65243 ba5ce07e06a7
parent 64858 e31cf6eaecb8
child 65269 2947837b9f04
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Mar 14 21:24:33 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Mar 14 21:26:25 2017 +0100
     1.3 @@ -145,6 +145,6 @@
     1.4        GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) }
     1.5      if (change.deps_changed ||
     1.6          PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version.nodes).nonEmpty)
     1.7 -      PIDE.deps_changed()
     1.8 +      PIDE.plugin.deps_changed()
     1.9    }
    1.10  }