diff -r 9dfcde68b383 -r cf6625012282 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 21:10:03 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 21:32:48 2010 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 
-import scala.swing.{FlowPanel, Button, ToggleButton}
+import scala.swing.{FlowPanel, Button, CheckBox}
 import scala.swing.event.ButtonClicked
 
 import javax.swing.JPanel
@@ -59,7 +59,7 @@
     reactions += { case ButtonClicked(_) => handle_update() }
   }
 
-  val follow = new ToggleButton("Follow")
+  val follow = new CheckBox("Follow")
   follow.selected = true