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)) }