build
changeset 18321 3414557c2dda
parent 17649 631b99d49809
child 26211 ffd91f7a78a2
     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"