--- 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