--- a/src/Tools/jEdit/src/info_dockable.scala Wed Sep 18 13:31:44 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Wed Sep 18 15:09:15 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button}
+import scala.swing.Button
import scala.swing.event.ButtonClicked
import java.lang.System
@@ -94,7 +94,7 @@
private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
zoom.tooltip = "Zoom factor for basic font size"
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
+ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(zoom)
add(controls.peer, BorderLayout.NORTH)