| author | wenzelm |
| Sat, 20 Dec 2008 11:55:34 +0100 | |
| changeset 29145 | b1c6f4563df7 |
| parent 26576 | fc76b7b79ba9 |
| child 31310 | b5365a9db718 |
| permissions | -rw-r--r-- |
1 # -*- shell-script -*-
2 #
3 # Author: Makarius
4 #
5 # timestart - setup bash environment for timing.
6 #
8 TIMES_RESULT=""
10 function get_times () {
11 local TMP="/tmp/get_times$$"
12 times > "$TMP" # No pipe here!
13 TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") | perl -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')"
14 rm -f "$TMP"
15 }
17 get_times # sets TIMES_RESULT