ignore deps_changed (again) -- avoid proactive load attempts of unfinished header specification while the user is typing;
authorwenzelm
Tue, 08 Apr 2014 09:48:38 +0200
changeset 56460 af28fdd50690
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
--- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Apr 08 09:45:13 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Apr 08 09:48:38 2014 +0200
@@ -120,7 +120,6 @@
   override def commit(change: Session.Change)
   {
     if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
-    if (change.deps_changed) PIDE.deps_changed()
   }
 }