src/Tools/jEdit/src/output_dockable.scala

--- a/src/Tools/jEdit/src/output_dockable.scala	Thu May 08 00:14:06 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu May 08 11:47:38 2014 +0200
@@ -143,8 +143,7 @@
   }
 
   private val controls =
-    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-      auto_update, update, pretty_text_area.detach_button,
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
       pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }