src/Tools/jEdit/src/simplifier_trace_window.scala
changeset 56770 e160ae47db94
parent 56750 205dd4439db1
child 56782 433cf57550fa
     1.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Mon Apr 28 14:19:14 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Mon Apr 28 14:41:49 2014 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4  
     1.5    peer.addComponentListener(new ComponentAdapter {
     1.6      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     1.7 -    override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
     1.8 +    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
     1.9    })
    1.10  
    1.11