| author | wenzelm |
| Thu, 06 Jul 2006 11:26:49 +0200 | |
| changeset 20021 | 815393c02db9 |
| parent 18322 | 56554bb23eda |
| child 28467 | c8336c42668e |
| permissions | -rw-r--r-- |
|
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
1 |
# -*- shell-script -*- |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
2 |
# $Id$ |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
3 |
# Author: Makarius |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
4 |
# |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
5 |
# timestop - report timing based on environment (cf. timestart.bash) |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
6 |
# |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
7 |
|
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
8 |
TIMES_REPORT="" |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
9 |
|
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
10 |
function show_times () |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
11 |
{
|
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
12 |
local TIMES_START="$TIMES_RESULT" |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
13 |
get_times |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
14 |
local TIMES_STOP="$TIMES_RESULT" |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
15 |
local KIND |
| 18322 | 16 |
for KIND in 1 2 |
|
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
17 |
do |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
18 |
local START=$(echo "$TIMES_START" | cut -d " " -f $KIND) |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
19 |
local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND) |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
20 |
|
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
21 |
local TIME=$[ $STOP - $START ] |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
22 |
local SECS=$[ $TIME % 60 ] |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
23 |
[ $SECS -lt 10 ] && SECS="0$SECS" |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
24 |
local MINUTES=$[ ($TIME / 60) % 60 ] |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
25 |
[ $MINUTES -lt 10 ] && MINUTES="0$MINUTES" |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
26 |
local HOURS=$[ $TIME / 3600 ] |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
27 |
|
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
28 |
local KIND_NAME |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
29 |
[ "$KIND" = 1 ] && KIND_NAME="elapsed time" |
| 18322 | 30 |
[ "$KIND" = 2 ] && KIND_NAME="cpu time" |
|
18318
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
31 |
local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}"
|
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
32 |
|
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
33 |
if [ -z "$TIMES_REPORT" ]; then |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
34 |
TIMES_REPORT="$RESULT" |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
35 |
else |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
36 |
TIMES_REPORT="$TIMES_REPORT, $RESULT" |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
37 |
fi |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
38 |
done |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
39 |
} |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
40 |
|
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
41 |
show_times # sets TIMES_REPORT |
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
42 |
|
|
deb87d7e44bc
timestop - report timing based on environment (cf. timestart.bash);
wenzelm
parents:
diff
changeset
|
43 |
unset TIMES_RESULT get_times show_times |