src/Tools/jEdit/src/jedit_resources.scala
changeset 57622 2da79fca5708
parent 57612 990ffb84489b
child 57841 e212e2001b2a
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Jul 23 16:56:03 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Jul 23 18:04:16 2014 +0200
     1.3 @@ -114,6 +114,7 @@
     1.4    override def commit(change: Session.Change)
     1.5    {
     1.6      if (change.syntax_changed) GUI_Thread.later { jEdit.propertiesChanged() }
     1.7 +    if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
     1.8    }
     1.9  }
    1.10