# HG changeset patch
# User wenzelm
# Date 1689509516 -7200
# Node ID e33cca11b474bd6d5c88ba4e3cc356c29d56df7b
# Parent  fca9ec5a615c6aaba3c87289b9e067adab05cab0
clarified options;

diff -r fca9ec5a615c -r e33cca11b474 etc/options
--- a/etc/options	Sun Jul 16 13:45:46 2023 +0200
+++ b/etc/options	Sun Jul 16 14:11:56 2023 +0200
@@ -198,6 +198,9 @@
 option build_database_slice : real = 300
   -- "slice size in MiB for ML heap stored within database"
 
+option build_delay : real = 0.2
+  -- "delay build process main loop"
+
 
 section "Editor Session"
 
diff -r fca9ec5a615c -r e33cca11b474 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Jul 16 13:45:46 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Jul 16 14:11:56 2023 +0200
@@ -1071,7 +1071,7 @@
 
     def sleep(): Unit =
       Isabelle_Thread.interrupt_handler(_ => progress.stop()) {
-        build_options.seconds("editor_input_delay").sleep()
+        build_options.seconds("build_delay").sleep()
       }
 
     def start_job(): Boolean = synchronized_database("Build_Process.start_job") {