diff --git a/bench_primes.sh b/bench_primes.sh new file mode 100644 index 00000000..52b618c5 --- /dev/null +++ b/bench_primes.sh @@ -0,0 +1,3 @@ +#!/bin/sh +OPTS="--profile=release --display=quiet" +exec dune exec $OPTS -- benchs/primes.exe $@