src/Tools/jEdit/src/output_dockable.scala
changeset 66206 2d2082db735a
parent 66205 e9fa94f43a15
child 66591 6efa351190d0
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Jun 27 21:36:58 2017 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Jun 27 21:56:56 2017 +0200
@@ -106,8 +106,7 @@
   private val controls =
     Wrap_Panel(
       List(output_state_button, auto_update_button,
-        update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom),
-      Wrap_Panel.Alignment.Right)
+        update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
 
   add(controls.peer, BorderLayout.NORTH)