Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lib/scripts/timestart.bash
author wenzelm
Sat, 20 Dec 2008 11:55:34 +0100
changeset 29145 b1c6f4563df7
parent 26576 fc76b7b79ba9
child 31310 b5365a9db718
permissions -rw-r--r--
removed Ids;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18317
bab988e37393 timestart - setup bash environment for timing;
wenzelm
parents:
diff changeset 
     1
 
# -*- shell-script -*-
29145
b1c6f4563df7 removed Ids;
wenzelm
parents: 26576
diff changeset 
     2
 
#
18317
bab988e37393 timestart - setup bash environment for timing;
wenzelm
parents:
diff changeset 
     3
 
# Author: Makarius
bab988e37393 timestart - setup bash environment for timing;
wenzelm
parents:
diff changeset 
     4
 
#
bab988e37393 timestart - setup bash environment for timing;
wenzelm
parents:
diff changeset 
     5
 
# timestart - setup bash environment for timing.
bab988e37393 timestart - setup bash environment for timing;
wenzelm
parents:
diff changeset 
     6
 
#
bab988e37393 timestart - setup bash environment for timing;
wenzelm
parents:
diff changeset 
     7
 












bab988e37393
timestart - setup bash environment for timing;



wenzelm


parents: 

diff
changeset




     8


TIMES_RESULT=""













bab988e37393
timestart - setup bash environment for timing;



wenzelm


parents: 

diff
changeset




     9














bab988e37393
timestart - setup bash environment for timing;



wenzelm


parents: 

diff
changeset




    10


function get_times () {













bab988e37393
timestart - setup bash environment for timing;



wenzelm


parents: 

diff
changeset




    11


  local TMP="/tmp/get_times$$"













bab988e37393
timestart - setup bash environment for timing;



wenzelm


parents: 

diff
changeset




    12


  times > "$TMP"   # No pipe here!








26576






fc76b7b79ba9
removed obsolete AUTO_PERL feature;



wenzelm


parents: 
18364

diff
changeset




    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')"








18327





wenzelm


parents: 
18322

diff
changeset




    14


  rm -f "$TMP"








18317






bab988e37393
timestart - setup bash environment for timing;



wenzelm


parents: 

diff
changeset




    15


}













bab988e37393
timestart - setup bash environment for timing;



wenzelm


parents: 

diff
changeset




    16














bab988e37393
timestart - setup bash environment for timing;



wenzelm


parents: 

diff
changeset




    17


get_times  # sets TIMES_RESULT















isabelle