10 if $
(which gtime
) --version >/dev
/null
2>&1; then
12 elif $
(which gnutime
) --version >/dev
/null
2>&1; then
14 elif $
(which time) --version 2>&1 |
grep -q GNU
; then
17 die
'Can'\''t find GNU time'
23 bench
="string-concat vector-concat"
26 for prog
in $bench; do
32 ( cat $prog.sml
; echo "val _ = Main.doit (valOf (Int.fromString (hd (CommandLine.arguments ()))))" ) > $prog.main.sml
33 mlton
-output $prog $prog.main.sml
1>/dev
/null
2>/dev
/null
38 while [ "$(echo "$t < $minTime" | bc)" = "1" ]; do
43 elif [ $n -lt $m ]; then
54 $time -o $prog.
time --format "%U + %S" .
/$prog $n 1>/dev
/null
2>/dev
/null
55 t
=$
(cat $prog.
time |
grep -v "Command exited" |
bc)
56 s
=$
(grep "Command exited" $prog.
time)
57 if [ ! -z "$s" ]; then
63 echo "(\"$prog\", $n):: (* $t sec $s*)"
65 rm $prog $prog.main.sml
$prog.
time