Merge pull request #4363 from jacereda/master
Fix shell return code, closes #4362
commit86615f026b42b21d6f2461417a063a985f0f4033
authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com>
dateFri 9 Mar 2018, 11:59 (9 years ago)
parentb5c22c04b04d93
benchmarks/build.pl+1−1
@@ -8,7 +8,7 @@ foreach $b (@bm) {
88 print "Building $1 / $2\n";
99 chdir $1;
1010 system("idris --clean $2.ipkg");
11− system("idris --build $2.ipkg");
11+ system("idris --build $2.ipkg") == 0 or die "Unable to build $2: $?";
1212 chdir "..";
1313 }
1414}