src/Tools/jEdit/src/output_dockable.scala

--- a/src/Tools/jEdit/src/output_dockable.scala	Wed May 21 14:09:43 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed May 21 14:42:45 2014 +0200
@@ -144,6 +144,6 @@
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
-      pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
+      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }