# HG changeset patch
# User wenzelm
# Date 1406131456 -7200
# Node ID 2da79fca57089c0bb41dfa02575891d6fe461989
# Parent  caa37976801f35d5c9ae1d597999de504a1bd99b
another attempt at more aggressive auto-loading (amending af28fdd50690) -- hidden buffers are now suppressed;

diff -r caa37976801f -r 2da79fca5708 src/Tools/jEdit/src/jedit_resources.scala
--- 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()
   }
 }