# HG changeset patch
# User wenzelm
# Date 1457693361 -3600
# Node ID 092c63734cc656811ff150f956c6995634f302ed
# Parent  75452e3eda14637c99281a073c01a68b9ae945fa
tuned message;

diff -r 75452e3eda14 -r 092c63734cc6 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Mar 11 08:39:57 2016 +0100
+++ b/src/Pure/Tools/build.scala	Fri Mar 11 11:49:21 2016 +0100
@@ -1102,10 +1102,8 @@
       val sessions = getopts(args)
 
       val progress = new Console_Progress(verbose)
-      val start_time = Time.now()
-      val show_timing = !no_build && verbose
 
-      if (show_timing) {
+      if (verbose) {
         progress.echo(
           Library.trim_line(
             Isabelle_System.bash(
@@ -1113,25 +1111,25 @@
         progress.echo(show_settings())
       }
 
+      val start_time = Time.now()
       val results =
         progress.interrupt_handler {
           build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
             dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
             check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
         }
+      val elapsed_time = Time.now() - start_time
 
-      if (show_timing) {
-        val elapsed_time = Time.now() - start_time
-
+      if (verbose) {
         progress.echo(
           Library.trim_line(
             Isabelle_System.bash("""echo "Finished at "; date""").out))
+      }
 
-        val total_timing =
-          (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
-            copy(elapsed = elapsed_time)
-        progress.echo(total_timing.message_resources)
-      }
+      val total_timing =
+        (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
+          copy(elapsed = elapsed_time)
+      progress.echo(total_timing.message_resources)
 
       results.rc
     }