diff --git a/tools/perf.sh b/tools/perf.sh index d3d742797..918909abd 100755 --- a/tools/perf.sh +++ b/tools/perf.sh @@ -17,5 +17,16 @@ ITERS=$1 ENGINE=$2 BENCHMARK=$3 +PRINT_MIN=$4 -( ( for i in `seq 1 1 $ITERS`; do time "$ENGINE" "$BENCHMARK"; done ) 2>&1 ) | grep user | sed 's/user[ \t]*\([0-9]*\)m\([0-9.]*\)s/\1 \2/g' | awk '{ s += $1 * 60 + $2; n += 1; } END { print s / n; }' +perf_values=$(( ( for i in `seq 1 1 $ITERS`; do time "$ENGINE" "$BENCHMARK"; done ) 2>&1 ) | \ + grep user | \ + sed 's/user[ \t]*\([0-9]*\)m\([0-9.]*\)s/\1 \2/g' | \ + awk 'BEGIN { min_v = -1; } { v = $1 * 60 + $2; if (min_v == -1 || v < min_v) { min_v = v; }; s += v; n += 1; } END { print s / n, min_v; }'); + +if [ "$PRINT_MIN" == "-min" ] +then + echo $perf_values | cut -d ' ' -f 2 +else + echo $perf_values | cut -d ' ' -f 1 +fi