# HG changeset patch
# User wenzelm
# Date 1396943318 -7200
# Node ID af28fdd506901b0d555671abbf0cad46ec997319
# Parent  38d0b209974307bce0690a19cfaa3808aff6f462
ignore deps_changed (again) -- avoid proactive load attempts of unfinished header specification while the user is typing;

diff -r 38d0b2099743 -r af28fdd50690 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()
   }
 }