src/Pure/mk
changeset 18321 3414557c2dda
parent 16376 65e2df6d8e10
child 20776 cc436bcdd5fc
     1.1 --- a/src/Pure/mk	Thu Dec 01 18:41:44 2005 +0100
     1.2 +++ b/src/Pure/mk	Thu Dec 01 18:41:46 2005 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4  
     1.5  # run isabelle
     1.6  
     1.7 -SECONDS=0
     1.8 +. "$ISABELLE_HOME/lib/scripts/timestart.bash"
     1.9  
    1.10  if [ -z "$RAW" ]; then
    1.11    ITEM="Pure"
    1.12 @@ -107,13 +107,13 @@
    1.13    RC="$?"
    1.14  fi
    1.15  
    1.16 -ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
    1.17 +. "$ISABELLE_HOME/lib/scripts/timestop.bash"
    1.18  
    1.19  
    1.20  # exit status
    1.21  
    1.22  if [ "$RC" -eq 0 ]; then
    1.23 -  echo "Finished $ITEM ($ELAPSED elapsed time)"
    1.24 +  echo "Finished $ITEM ($TIMES_REPORT)"
    1.25    gzip --force "$LOG"
    1.26  else
    1.27    echo "$ITEM FAILED"