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)