ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-17 11:47:20 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #4363 from jacereda/master

Browse Source 
Fix shell return code, closes #4362
This commit is contained in:
Jan de Muijnck-Hughes 2018-03-09 11:59:09 +00:00 committed by GitHub
commit 86615f026b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
benchmarks/build.pl
View File

@ -8,7 +8,7 @@ foreach $b (@bm) {
print "Building $1 / $2\n";
chdir $1;
system("idris --clean $2.ipkg");
system("idris --build $2.ipkg");
system("idris --build $2.ipkg") == 0 or die "Unable to build $2: $?";
chdir "..";
}
}