author | wenzelm |
Sat, 11 Jul 2020 18:19:08 +0200 | |
changeset 72022 | 45865bb06182 |
parent 72021 | 664e90313a54 |
child 72023 | 08348e364739 |
--- 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 {