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)"