# HG changeset patch
# User wenzelm
# Date 1344791307 -7200
# Node ID 49a965020394b1be376ad7bac73a6fc169eb16e3
# Parent  71136069089da0b208d81559ab598c9723f86660
always show some timing information, to reduce the need for explicit -v;

diff -r 71136069089d -r 49a965020394 lib/Tools/build
--- a/lib/Tools/build	Sun Aug 12 17:39:06 2012 +0200
+++ b/lib/Tools/build	Sun Aug 12 19:08:27 2012 +0200
@@ -125,9 +125,10 @@
 
   show_settings ""
   echo
-  . "$ISABELLE_HOME/lib/scripts/timestart.bash"
 fi
 
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
+
 "$ISABELLE_TOOL" java isabelle.Build \
   "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
   "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
@@ -138,8 +139,9 @@
 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
   echo -n "Finished at "; date
 
-  . "$ISABELLE_HOME/lib/scripts/timestop.bash"
-  echo "$TIMES_REPORT"
 fi
 
+. "$ISABELLE_HOME/lib/scripts/timestop.bash"
+echo "$TIMES_REPORT"
+
 exit "$RC"