always show some timing information, to reduce the need for explicit -v;
authorwenzelm
Sun, 12 Aug 2012 19:08:27 +0200
changeset 48780 49a965020394
parent 48779 71136069089d
child 48781 21af4b8103fa
always show some timing information, to reduce the need for explicit -v;
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"