diff options
Diffstat (limited to 'scripts')
| -rwxr-xr-x | scripts/build-remote.pl.in | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/scripts/build-remote.pl.in b/scripts/build-remote.pl.in index 413d0402bf7a..a4eee75d1b17 100755 --- a/scripts/build-remote.pl.in +++ b/scripts/build-remote.pl.in @@ -46,7 +46,7 @@ sub all { $_ || return 0 for @_; 1 } # Initialisation. my $loadIncreased = 0; -my ($localSystem, $printBuildTrace) = @ARGV; +my ($localSystem, $maxSilentTime, $printBuildTrace, $buildTimeout) = @ARGV; my $currentLoad = $ENV{"NIX_CURRENT_LOAD"}; my $conf = $ENV{"NIX_REMOTE_SYSTEMS"}; @@ -261,7 +261,8 @@ close UPLOADLOCK; # Perform the build. my $buildFlags = - " --fallback --add-root $rootsDir/\$PPID.out --quiet" + "--max-silent-time $maxSilentTime --option build-timeout $buildTimeout" + . " --fallback --add-root $rootsDir/\$PPID.out --quiet" . " --option build-keep-log false"; # We let the remote side kill its process group when the connection is |