equal
deleted
inserted
replaced
32 local KIND_NAME |
32 local KIND_NAME |
33 [ "$KIND" = 1 ] && KIND_NAME="elapsed time" |
33 [ "$KIND" = 1 ] && KIND_NAME="elapsed time" |
34 [ "$KIND" = 2 ] && KIND_NAME="cpu time" |
34 [ "$KIND" = 2 ] && KIND_NAME="cpu time" |
35 local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}" |
35 local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}" |
36 |
36 |
37 if [ -z "$TIMES_REPORT" ]; then |
37 if [ ${KIND} -eq 1 -o ${TIME} -ge 5 ]; then |
38 TIMES_REPORT="$RESULT" |
38 if [ -z "$TIMES_REPORT" ]; then |
39 else |
39 TIMES_REPORT="$RESULT" |
40 TIMES_REPORT="$TIMES_REPORT, $RESULT" |
40 else |
|
41 TIMES_REPORT="$TIMES_REPORT, $RESULT" |
|
42 fi |
41 fi |
43 fi |
42 done |
44 done |
43 if let "$TIME1 >= 5 && $TIME2 >= 5" |
45 if let "$TIME1 >= 5 && $TIME2 >= 5" |
44 then |
46 then |
45 local FACTOR=$(( $TIME2 * 100 / $TIME1 )) |
47 local FACTOR=$(( $TIME2 * 100 / $TIME1 )) |