Adding '-min' option to tools/perf.sh: the option switches to output of minimum instead of average of performance measurements.

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