etc/options
changeset 73701 d83e7e444b43
parent 73691 2f9877db82a1
child 73721 52030acb19ac
--- a/etc/options	Sun May 16 13:06:13 2021 +0200
+++ b/etc/options	Sun May 16 13:14:16 2021 +0200
@@ -113,6 +113,9 @@
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
+option timeout_build : bool = true
+  -- "observe timeout for session build"
+
 option process_output_limit : int = 100
   -- "build process output limit (in million characters, 0 = unlimited)"