# HG changeset patch
# User wenzelm
# Date 1274433174 -7200
# Node ID 0e4073f19825b34127798b3beb87b1bc7c7caa3d
# Parent  58a0757031dd6e62768ee7ada1afb2fa4e0099a2
component resize: full handle_resize;

diff -r 58a0757031dd -r 0e4073f19825 src/Tools/jEdit/src/jedit/output_dockable.scala
--- 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() }
   })