replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
authorwenzelm
Thu Dec 01 18:41:46 2005 +0100 (2005-12-01)
changeset 183213414557c2dda
parent 18320 ce523820ff75
child 18322 56554bb23eda
replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
build
lib/Tools/makeall
lib/Tools/usedir
src/Pure/mk
     1.1 --- a/build	Thu Dec 01 18:41:44 2005 +0100
     1.2 +++ b/build	Thu Dec 01 18:41:46 2005 +0100
     1.3 @@ -169,8 +169,8 @@
     1.4  
     1.5  # build it
     1.6  
     1.7 -SECONDS=0
     1.8  echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
     1.9 +. "$ISABELLE_HOME/lib/scripts/timestart.bash"
    1.10  
    1.11  for L in $MAKE_LOGICS
    1.12  do
    1.13 @@ -179,5 +179,5 @@
    1.14  
    1.15  echo -n "Finished at "; date
    1.16  
    1.17 -ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
    1.18 -echo "$ELAPSED total elapsed time"
    1.19 +. "$ISABELLE_HOME/lib/scripts/timestop.bash"
    1.20 +echo "$TIMES_REPORT"
     2.1 --- a/lib/Tools/makeall	Thu Dec 01 18:41:44 2005 +0100
     2.2 +++ b/lib/Tools/makeall	Thu Dec 01 18:41:46 2005 +0100
     2.3 @@ -37,6 +37,7 @@
     2.4  FAIL=""
     2.5  
     2.6  echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
     2.7 +. "$ISABELLE_HOME/lib/scripts/timestart.bash"
     2.8  
     2.9  for L in $ALL_LOGICS
    2.10  do
    2.11 @@ -45,7 +46,7 @@
    2.12  
    2.13  echo -n "Finished at "; date
    2.14  
    2.15 -ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
    2.16 -echo "$ELAPSED total elapsed time"
    2.17 +. "$ISABELLE_HOME/lib/scripts/timestop.bash"
    2.18 +echo "$TIMES_REPORT"
    2.19  
    2.20  [ "$FAIL" = "" ] || fail "Logics ${FAIL}FAILED!"
     3.1 --- a/lib/Tools/usedir	Thu Dec 01 18:41:44 2005 +0100
     3.2 +++ b/lib/Tools/usedir	Thu Dec 01 18:41:46 2005 +0100
     3.3 @@ -198,7 +198,7 @@
     3.4  fi
     3.5  
     3.6  
     3.7 -SECONDS=0
     3.8 +. "$ISABELLE_HOME/lib/scripts/timestart.bash"
     3.9  
    3.10  if [ -n "$BUILD" ]; then
    3.11    ITEM="$SESSION"
    3.12 @@ -224,13 +224,13 @@
    3.13    cd ..
    3.14  fi
    3.15  
    3.16 -ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
    3.17 +. "$ISABELLE_HOME/lib/scripts/timestop.bash"
    3.18  
    3.19  
    3.20  # exit status
    3.21  
    3.22  if [ "$RC" -eq 0 ]; then
    3.23 -  echo "Finished $ITEM ($ELAPSED elapsed time)" >&2
    3.24 +  echo "Finished $ITEM ($TIMES_REPORT)" >&2
    3.25    gzip --force "$LOG"
    3.26  else
    3.27    { echo "$ITEM FAILED";
     4.1 --- a/src/Pure/mk	Thu Dec 01 18:41:44 2005 +0100
     4.2 +++ b/src/Pure/mk	Thu Dec 01 18:41:46 2005 +0100
     4.3 @@ -81,7 +81,7 @@
     4.4  
     4.5  # run isabelle
     4.6  
     4.7 -SECONDS=0
     4.8 +. "$ISABELLE_HOME/lib/scripts/timestart.bash"
     4.9  
    4.10  if [ -z "$RAW" ]; then
    4.11    ITEM="Pure"
    4.12 @@ -107,13 +107,13 @@
    4.13    RC="$?"
    4.14  fi
    4.15  
    4.16 -ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
    4.17 +. "$ISABELLE_HOME/lib/scripts/timestop.bash"
    4.18  
    4.19  
    4.20  # exit status
    4.21  
    4.22  if [ "$RC" -eq 0 ]; then
    4.23 -  echo "Finished $ITEM ($ELAPSED elapsed time)"
    4.24 +  echo "Finished $ITEM ($TIMES_REPORT)"
    4.25    gzip --force "$LOG"
    4.26  else
    4.27    echo "$ITEM FAILED"