# HG changeset patch
# User wenzelm
# Date 1594484348 -7200
# Node ID 45865bb06182f2a0c8905291a9bef0e63db3bb5e
# Parent  664e90313a5403cdfebdea300d01b7c39b5cf821
clarified message --- as in former ML version (see 940195fbb282);

diff -r 664e90313a54 -r 45865bb06182 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jul 11 17:15:28 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 11 18:19:08 2020 +0200
@@ -681,9 +681,8 @@
             // messages
             process_result.err_lines.foreach(progress.echo)
 
-            if (verbose) progress.echo(session_timing(session_name, build_log))
-
             if (process_result.ok) {
+              if (verbose) progress.echo(session_timing(session_name, build_log))
               progress.echo(session_finished(session_name, process_result))
             }
             else {