# HG changeset patch
# User wenzelm
# Date 1375963984 -7200
# Node ID 288896518cf52abb2c2eca058c54d92512b505ee
# Parent  6c89225ddeba84dfe094af039185952b2037e0d3
tuned imports;

diff -r 6c89225ddeba -r 288896518cf5 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Wed Aug 07 23:20:11 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Thu Aug 08 14:13:04 2013 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 
-import scala.swing.{FlowPanel, Button, CheckBox}
+import scala.swing.{FlowPanel, Button}
 import scala.swing.event.ButtonClicked
 
 import java.lang.System