on master help sign in
Read idris executable from environment variable
commit25baedb7d8634075543ad0a61c9e8eb08b8bf6a2 authorJorge Acereda <jacereda@gmail.com> dateFri 23 Mar 2018, 13:32 (9 years ago) parent425700d
1 file changed+3−2
benchmarks/build.pl+3−2
benchmarks/build.pl+3−2
@@ -2,13 +2,14 @@
22
33$bmarks = `cat ALL`;
44@bm = split(/\n/, $bmarks);
5+$idris = $ENV{'IDRIS'} || "idris";
56
67foreach $b (@bm) {
78 if ($b =~ /([a-zA-Z0-9]+)\/([a-zA-Z0-9]+)\s+(.*)/) {
89 print "Building $1 / $2\n";
910 chdir $1;
10− system("idris --clean $2.ipkg");
11− system("idris --build $2.ipkg") == 0 or die "Unable to build $2: $?";
11+ system("$idris --clean $2.ipkg");
12+ system("$idris --build $2.ipkg") == 0 or die "Unable to build $2: $?";
1213 chdir "..";
1314 }
1415}