etc/options
changeset 83209 a39fde2f020a
parent 83201 d3220d015c9d
child 83223 a225609e3344
--- a/etc/options	Sun Sep 21 19:47:26 2025 +0200
+++ b/etc/options	Sun Sep 21 23:48:59 2025 +0200
@@ -212,6 +212,9 @@
 option build_database_slice : real = 300 for build_sync
   -- "slice size in MiB for ML heap stored within database"
 
+option build_progress_delay : real = 2
+  -- "delay for detailed build progress"
+
 option build_delay : real = 0.2
   -- "delay for build process main loop (local)"