tuned;
authorwenzelm
Sat, 26 Apr 2014 14:59:50 +0200
changeset 56750 205dd4439db1
parent 56749 e96d6b38649e
child 56751 2080e752ed40
tuned;
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 += {