equal
deleted
inserted
replaced
11 { |
11 { |
12 local TIMES_START="$TIMES_RESULT" |
12 local TIMES_START="$TIMES_RESULT" |
13 get_times |
13 get_times |
14 local TIMES_STOP="$TIMES_RESULT" |
14 local TIMES_STOP="$TIMES_RESULT" |
15 local KIND |
15 local KIND |
16 for KIND in 1 2 3 |
16 for KIND in 1 2 |
17 do |
17 do |
18 local START=$(echo "$TIMES_START" | cut -d " " -f $KIND) |
18 local START=$(echo "$TIMES_START" | cut -d " " -f $KIND) |
19 local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND) |
19 local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND) |
20 |
20 |
21 local TIME=$[ $STOP - $START ] |
21 local TIME=$[ $STOP - $START ] |
25 [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES" |
25 [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES" |
26 local HOURS=$[ $TIME / 3600 ] |
26 local HOURS=$[ $TIME / 3600 ] |
27 |
27 |
28 local KIND_NAME |
28 local KIND_NAME |
29 [ "$KIND" = 1 ] && KIND_NAME="elapsed time" |
29 [ "$KIND" = 1 ] && KIND_NAME="elapsed time" |
30 [ "$KIND" = 2 ] && KIND_NAME="user" |
30 [ "$KIND" = 2 ] && KIND_NAME="cpu time" |
31 [ "$KIND" = 3 ] && KIND_NAME="system" |
|
32 local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}" |
31 local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}" |
33 |
32 |
34 if [ -z "$TIMES_REPORT" ]; then |
33 if [ -z "$TIMES_REPORT" ]; then |
35 TIMES_REPORT="$RESULT" |
34 TIMES_REPORT="$RESULT" |
36 else |
35 else |