ignore deps_changed (again) -- avoid proactive load attempts of unfinished header specification while the user is typing;
authorwenzelm
Tue Apr 08 09:48:38 2014 +0200 (2014-04-08)
changeset 56460af28fdd50690
parent 56459 38d0b2099743
child 56461 ae33d153f6cc
ignore deps_changed (again) -- avoid proactive load attempts of unfinished header specification while the user is typing;
src/Tools/jEdit/src/jedit_resources.scala
     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