src/Tools/jEdit/src/simplifier_trace_window.scala
changeset 56750 205dd4439db1
parent 56662 f373fb77e0a4
child 56770 e160ae47db94
     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 += {