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"