src/Tools/jEdit/src/jedit_resources.scala
changeset 56460 af28fdd50690
parent 56457 eea4bbe15745
child 56502 db2836f65d42
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Apr 08 09:45:13 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Apr 08 09:48:38 2014 +0200
     1.3 @@ -120,7 +120,6 @@
     1.4    override def commit(change: Session.Change)
     1.5    {
     1.6      if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
     1.7 -    if (change.deps_changed) PIDE.deps_changed()
     1.8    }
     1.9  }
    1.10