# HG changeset patch
# User wenzelm
# Date 1398517190 -7200
# Node ID 205dd4439db19cb0e1d7c1f14442fb535470f934
# Parent  e96d6b38649ed0b9efb1c96bbcea23b509b1b83d
tuned;

diff -r e96d6b38649e -r 205dd4439db1 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Sat Apr 26 14:01:06 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Sat Apr 26 14:59:50 2014 +0200
@@ -207,9 +207,7 @@
   val use_regex = new CheckBox("Regex")
 
   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-    new Label {
-      text = "Search"
-    },
+    new Label("Search"),
     new TextField(30) {
       listenTo(keys)
       reactions += {