max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/playground/run.sh): fix

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-27 10:57:36 +01:00
parent ed4cd39d59
commit 467799c6c3
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/playground/run.sh
View file

@ -3,6 +3,7 @@ if [ $# -eq 0 ]; then
echo "Usage: run.sh [file] [args]*"
exit 1
fi
./compile.sh $1
ff=$1
./compile.sh $ff
shift 1
"./$ff.out" $*
time "./$ff.out" $*