src/Pure/Tools/build.scala
changeset 72019 940195fbb282
parent 72018 5c9984820caa
child 72021 664e90313a54
--- a/src/Pure/Tools/build.scala	Sat Jul 11 16:41:55 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 11 16:58:38 2020 +0200
@@ -681,6 +681,8 @@
             // messages
             process_result.err_lines.foreach(progress.echo)
 
+            if (verbose) progress.echo(session_timing(session_name, build_log.session_timing))
+
             if (process_result.ok) {
               progress.echo(session_finished(session_name, process_result.timing))
             }