# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1710422444 -3600
# Node ID 3acbfeec4a95bec9aaa5e1abf8d130adaa612f89
# Parent  7ea70796acaa317b706c4d93751320bdb6f6dedc
more synced options (following 6e5397fcc41b);

diff -r 7ea70796acaa -r 3acbfeec4a95 etc/options
--- a/etc/options	Thu Mar 14 08:24:48 2024 +0000
+++ b/etc/options	Thu Mar 14 14:20:44 2024 +0100
@@ -144,7 +144,7 @@
 option timeout : real = 0 for build
   -- "timeout for session build job (seconds > 0)"
 
-option timeout_build : bool = true for build
+option timeout_build : bool = true for build build_sync
   -- "observe timeout for session build"
 
 option process_policy : string = ""
@@ -198,7 +198,7 @@
 option build_database : bool = false for build_sync
   -- "expose state of build process via central database"
 
-option build_database_slice : real = 300
+option build_database_slice : real = 300 for build_sync
   -- "slice size in MiB for ML heap stored within database"
 
 option build_delay : real = 0.2