| author | wenzelm | 
| Wed, 23 Jul 2014 18:04:16 +0200 | |
| changeset 57622 | 2da79fca5708 | 
| parent 57621 | caa37976801f | 
| child 57623 | 249c0297cf10 | 
--- a/src/Tools/jEdit/src/jedit_resources.scala Wed Jul 23 16:56:03 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Jul 23 18:04:16 2014 +0200 @@ -114,6 +114,7 @@ override def commit(change: Session.Change) { if (change.syntax_changed) GUI_Thread.later { jEdit.propertiesChanged() } + if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed() } }