| changeset 18317 | bab988e37393 |
| child 18322 | 56554bb23eda |
| 18316:4b62e0cb3aa8 | 18317:bab988e37393 |
|---|---|
1 # -*- shell-script -*- |
|
2 # $Id$ |
|
3 # Author: Makarius |
|
4 # |
|
5 # timestart - setup bash environment for timing. |
|
6 # |
|
7 |
|
8 TIMES_RESULT="" |
|
9 |
|
10 #set by configure |
|
11 AUTO_PERL=perl |
|
12 |
|
13 function get_times () { |
|
14 local TMP="/tmp/get_times$$" |
|
15 times > "$TMP" # No pipe here! |
|
16 TIMES_RESULT="$SECONDS $(tail -1 "$TMP" | "$AUTO_PERL" -pe 's,(\d+)m(\d+)\.\d+s, $1 * 60 + $2,ge')" |
|
17 /bin/rm -f "$TMP" |
|
18 } |
|
19 |
|
20 get_times # sets TIMES_RESULT |
|
21 |