changeset 80645 | a1dce0cc6c26 |
parent 80471 | 12901c03b416 |
child 81224 | 6922f189cb43 |
--- a/etc/options Tue Aug 06 13:54:10 2024 +0200 +++ b/etc/options Tue Aug 06 15:00:37 2024 +0200 @@ -252,6 +252,9 @@ option build_manager_timeout : real = 28800 -- "timeout for user-submitted tasks (seconds > 0)" +option build_manager_cancel_timeout : real = 180.0 + -- "timeout for graceful cancelling (seconds > 0)" + option build_manager_delay : real = 1.0 -- "delay build manager loop"