| author | wenzelm |
| Sun, 31 May 2009 14:20:54 +0200 | |
| changeset 31310 | b5365a9db718 |
| parent 29145 | b1c6f4563df7 |
| permissions | -rw-r--r-- |
| wenzelm@31310 | 1 |
# -*- shell-script -*- :mode=shellscript: |
| wenzelm@29145 | 2 |
# |
| wenzelm@18317 | 3 |
# Author: Makarius |
| wenzelm@18317 | 4 |
# |
| wenzelm@18317 | 5 |
# timestart - setup bash environment for timing. |
| wenzelm@18317 | 6 |
# |
| wenzelm@18317 | 7 |
|
| wenzelm@18317 | 8 |
TIMES_RESULT="" |
| wenzelm@18317 | 9 |
|
| wenzelm@18317 | 10 |
function get_times () {
|
| wenzelm@18317 | 11 |
local TMP="/tmp/get_times$$" |
| wenzelm@18317 | 12 |
times > "$TMP" # No pipe here! |
| wenzelm@26576 | 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')" |
| wenzelm@18327 | 14 |
rm -f "$TMP" |
| wenzelm@18317 | 15 |
} |
| wenzelm@18317 | 16 |
|
| wenzelm@18317 | 17 |
get_times # sets TIMES_RESULT |