lib/scripts/timestart.bash
changeset 18317 bab988e37393
child 18322 56554bb23eda
equal deleted inserted replaced
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