src/Tools/jEdit/src/jedit/output_dockable.scala

--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 27 12:34:30 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 27 12:35:40 2010 +0200
@@ -106,7 +106,7 @@
   /* resize */
 
   addComponentListener(new ComponentAdapter {
-    val delay = Swing_Thread.delay_last(500) { handle_resize() }
+    val delay = Swing_Thread.delay_last(500) { handle_resize() }  // FIXME update_delay property
     override def componentResized(e: ComponentEvent) { delay() }
   })