--- a/lib/Tools/makeall Thu Dec 01 18:41:44 2005 +0100
+++ b/lib/Tools/makeall Thu Dec 01 18:41:46 2005 +0100
@@ -37,6 +37,7 @@
FAIL=""
echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
for L in $ALL_LOGICS
do
@@ -45,7 +46,7 @@
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"
[ "$FAIL" = "" ] || fail "Logics ${FAIL}FAILED!"