ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-10-26 09:54:23 +03:00
Code Issues Projects Releases Wiki Activity

Read idris executable from environment variable

Browse Source
This commit is contained in:
Jorge Acereda 2018-03-23 13:32:12 +01:00
parent 425700d9e8
commit 25baedb7d8
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
benchmarks/build.pl
View File

@ -2,13 +2,14 @@
$bmarks = `cat ALL`;
@bm = split(/\n/, $bmarks);
$idris = $ENV{'IDRIS'} || "idris";
foreach $b (@bm) {
if ($b =~ /([a-zA-Z0-9]+)\/([a-zA-Z0-9]+)\s+(.*)/) {
print "Building $1 / $2\n";
chdir $1;
system("idris --clean $2.ipkg");
system("idris --build $2.ipkg") == 0 or die "Unable to build $2: $?";
system("$idris --clean $2.ipkg");
system("$idris --build $2.ipkg") == 0 or die "Unable to build $2: $?";
chdir "..";
}
}