--- a/src/Tools/jEdit/src/info_dockable.scala Sun Nov 25 21:10:29 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Sun Nov 25 21:23:20 2012 +0100
@@ -115,8 +115,7 @@
/* resize */
private val delay_resize =
- Swing_Thread.delay_first(
- Time.seconds(PIDE.options.real("editor_update_delay"))) { handle_resize() }
+ Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }