etc/options
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"