observe follow_caret (again);
authorwenzelm
Tue, 20 Jul 2010 11:11:15 +0200
changeset 37850 afb5653a3a47
parent 37849 4f9de312cc23
child 37851 1ce77362598f
observe follow_caret (again);
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)
       }
     }