diff --git a/tests/playground/run.sh b/tests/playground/run.sh index 58973f580a..cdc955f8b5 100755 --- a/tests/playground/run.sh +++ b/tests/playground/run.sh @@ -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" $*