1.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 21:19:38 2010 -0700
     1.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 11:12:54 2010 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4    /* resize */
     1.5  
     1.6    addComponentListener(new ComponentAdapter {
     1.7 -    val delay = Swing_Thread.delay_last(500) { html_panel.refresh() }
     1.8 +    val delay = Swing_Thread.delay_last(500) { handle_resize() }
     1.9      override def componentResized(e: ComponentEvent) { delay() }
    1.10    })
    1.11