Give full path to time binary in benchmark

2023-09-16 21:35:06 +01:00 · 2023-09-16 21:35:06 +01:00 · d73107518c
parent 294576333c
commit d73107518c
1 changed files with 1 additions and 1 deletions
--- a/benchmark/benchmark.sh
+++ b/benchmark/benchmark.sh
@ -18,6 +18,6 @@ do
    done
 done

-TIMEFORMAT=%0R time ${@:1} > /dev/null
+TIMEFORMAT=%0R /usr/bin/time ${@:1} > /dev/null

 cd ../ && rm -rf temp/