etc/options
changeset 83316 6829b3579a54
parent 83303 416c05062d41
child 83506 b1e04ffb4b08
--- a/etc/options	Sun Oct 19 14:05:58 2025 +0200
+++ b/etc/options	Sun Oct 19 20:05:54 2025 +0200
@@ -212,10 +212,10 @@
 option build_database_slice : real = 300 for build_sync
   -- "slice size in MiB for ML heap stored within database"
 
-option build_progress_detailed : bool = false
+option build_progress_detailed : bool = false for build
   -- "enabled detailed build progress"
 
-option build_progress_delay : real = 2
+option build_progress_delay : real = 2 for build
   -- "delay for detailed build progress"
 
 option build_delay : real = 0.2