build

--- a/build	Thu Dec 01 18:41:44 2005 +0100
+++ b/build	Thu Dec 01 18:41:46 2005 +0100
@@ -169,8 +169,8 @@
 
 # build it
 
-SECONDS=0
 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
 for L in $MAKE_LOGICS
 do
@@ -179,5 +179,5 @@
 
 echo -n "Finished at "; date
 
-ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
-echo "$ELAPSED total elapsed time"
+. "$ISABELLE_HOME/lib/scripts/timestop.bash"
+echo "$TIMES_REPORT"