author | wenzelm |
Tue, 08 Apr 2014 09:48:38 +0200 | |
changeset 56460 | af28fdd50690 |
parent 56459 | 38d0b2099743 |
child 56461 | ae33d153f6cc |
--- 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() } }