etc/options
changeset 80469 a3bae6dd7344
parent 80459 00fcbb277dae
child 80470 f2f4b953ead6
--- a/etc/options	Mon Jul 01 14:46:51 2024 +0200
+++ b/etc/options	Mon Jul 01 15:24:04 2024 +0200
@@ -245,6 +245,9 @@
 
 option build_manager_cluster : string = "cluster.default"
 
+option build_manager_timeout : real = 28800
+  -- "timeout for user-submitted tasks (seconds > 0)"
+
 option build_manager_delay : real = 1.0
   -- "delay build manager loop"