--- a/src/Tools/jEdit/src/debugger_dockable.scala Thu Dec 08 22:11:36 2022 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Thu Dec 08 22:38:03 2022 +0100
@@ -339,7 +339,7 @@
/* resize */
private val delay_resize =
- Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
+ Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()