tuned;
authorwenzelm
Sat Apr 26 14:59:50 2014 +0200 (2014-04-26)
changeset 56750205dd4439db1
parent 56749 e96d6b38649e
child 56751 2080e752ed40
tuned;
src/Tools/jEdit/src/simplifier_trace_window.scala
     1.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Sat Apr 26 14:01:06 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Sat Apr 26 14:59:50 2014 +0200
     1.3 @@ -207,9 +207,7 @@
     1.4    val use_regex = new CheckBox("Regex")
     1.5  
     1.6    private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
     1.7 -    new Label {
     1.8 -      text = "Search"
     1.9 -    },
    1.10 +    new Label("Search"),
    1.11      new TextField(30) {
    1.12        listenTo(keys)
    1.13        reactions += {