--- 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"
--- 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!"
--- a/lib/Tools/usedir Thu Dec 01 18:41:44 2005 +0100
+++ b/lib/Tools/usedir Thu Dec 01 18:41:46 2005 +0100
@@ -198,7 +198,7 @@
fi
-SECONDS=0
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
if [ -n "$BUILD" ]; then
ITEM="$SESSION"
@@ -224,13 +224,13 @@
cd ..
fi
-ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
+. "$ISABELLE_HOME/lib/scripts/timestop.bash"
# exit status
if [ "$RC" -eq 0 ]; then
- echo "Finished $ITEM ($ELAPSED elapsed time)" >&2
+ echo "Finished $ITEM ($TIMES_REPORT)" >&2
gzip --force "$LOG"
else
{ echo "$ITEM FAILED";
--- a/src/Pure/mk Thu Dec 01 18:41:44 2005 +0100
+++ b/src/Pure/mk Thu Dec 01 18:41:46 2005 +0100
@@ -81,7 +81,7 @@
# run isabelle
-SECONDS=0
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
if [ -z "$RAW" ]; then
ITEM="Pure"
@@ -107,13 +107,13 @@
RC="$?"
fi
-ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
+. "$ISABELLE_HOME/lib/scripts/timestop.bash"
# exit status
if [ "$RC" -eq 0 ]; then
- echo "Finished $ITEM ($ELAPSED elapsed time)"
+ echo "Finished $ITEM ($TIMES_REPORT)"
gzip --force "$LOG"
else
echo "$ITEM FAILED"