changeset 37033 | 0e4073f19825 |
parent 37019 | 8f747cee4e27 |
child 37036 | 49559c4e85f9 |
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 21:19:38 2010 -0700 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Fri May 21 11:12:54 2010 +0200 @@ -111,7 +111,7 @@ /* resize */ addComponentListener(new ComponentAdapter { - val delay = Swing_Thread.delay_last(500) { html_panel.refresh() } + val delay = Swing_Thread.delay_last(500) { handle_resize() } override def componentResized(e: ComponentEvent) { delay() } })