author | wenzelm |
Sun, 31 May 2009 14:20:54 +0200 | |
changeset 31310 | b5365a9db718 |
parent 29145 | b1c6f4563df7 |
permissions | -rw-r--r-- |
1 # -*- shell-script -*- :mode=shellscript:
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