diff --git a/src/tools/make/buildall.pl b/src/tools/make/buildall.pl index 19d8fc80..3363bbc4 100755 --- a/src/tools/make/buildall.pl +++ b/src/tools/make/buildall.pl @@ -6,6 +6,8 @@ use Cwd; my $branch = "master"; +if (defined($ARGV[0]) && ($ARGV[0] ne "")) {$branch = $ARGV[0]} + my %machines = ( "pi" => ['pi@pie', "sudo", "projects/oberon/vishap/voc", "make full"], "darwin" => ['dave@dcb', "sudo", "projects/oberon/vishap/voc", "make full"], diff --git a/src/tools/make/postpush.pl b/src/tools/make/postpush.pl index 2b3a2ad6..85cde3b7 100755 --- a/src/tools/make/postpush.pl +++ b/src/tools/make/postpush.pl @@ -36,7 +36,6 @@ for my $file (@{$modified}) { if ($buildneeded) { writelog "Post push github web hook for repository $repo, branch $branch, name $name. Build required."; - my $child = fork; if (not defined $child) {die "Fork failed.";} if ($child) { @@ -45,7 +44,7 @@ if ($buildneeded) { close(STDIN); close(STDOUT); close(STDERR); # child process system 'echo Syncing voc>postpush.log'; system '(cd voc && git pull) >>postpush.log'; - exec 'perl voc/src/tools/make/buildall.pl >/tmp/buildall.log'; + exec 'perl voc/src/tools/make/buildall.pl $branch >/tmp/buildall.log'; exit; } } else {