author | wenzelm |
Sun, 06 Nov 2022 20:56:05 +0100 | |
changeset 76476 | 9600720071e6 |
parent 76475 | 5c7652e9bc01 |
child 76477 | 6e68ec0fdc48 |
--- a/src/Pure/Tools/build.scala Sun Nov 06 20:44:12 2022 +0100 +++ b/src/Pure/Tools/build.scala Sun Nov 06 20:56:05 2022 +0100 @@ -293,7 +293,9 @@ } def sleep(): Unit = - Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep() } + Isabelle_Thread.interrupt_handler(_ => progress.stop()) { + build_options.seconds("editor_input_delay").sleep() + } val log = build_options.string("system_log") match {