tools/times: tweaked shell script to work better

2012-11-27 07:24:18 +01:00 · 2012-11-27 07:24:18 +01:00 · b200e1c430
parent 1ebab4a442
commit b200e1c430
1 changed files with 1 additions and 1 deletions
--- a/tools/times.sh
+++ b/tools/times.sh
@ -14,7 +14,7 @@ make clean

 git reset --hard HEAD > times.log

-for i in {0..20}
+for i in 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
  do
    make CXXFLAGS=-O2 -j4
    echo "$i"