# HG changeset patch
# User wenzelm
# Date 1279617075 -7200
# Node ID afb5653a3a471d6c19c7dd1930f82c7e9235cc7b
# Parent  4f9de312cc23388eacb5733660a3d77bd268bbff
observe follow_caret (again);

diff -r 4f9de312cc23 -r afb5653a3a47 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Jul 19 22:19:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Tue Jul 20 11:11:15 2010 +0200
@@ -88,7 +88,7 @@
       react {
         case Session.Global_Settings => handle_resize()
         case Command_Set(changed) => handle_update(Some(changed))
-        case Session.Perspective => if (handle_perspective()) handle_update()
+        case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
         case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
       }
     }