diff -r a27747c85700 -r ab21876c30c1 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Mon May 25 22:37:22 2020 +0200 +++ b/src/Pure/Tools/dump.scala Tue May 26 11:17:10 2020 +0200 @@ -483,7 +483,7 @@ val start_date = Date.now() - if (verbose) progress.echo("Started at " + Build_Log.print_date(start_date)) + progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date)) progress.interrupt_handler { dump(options, logic, @@ -505,7 +505,7 @@ val end_date = Date.now() val timing = end_date.time - start_date.time - if (verbose) progress.echo("\nFinished at " + Build_Log.print_date(end_date)) + progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date)) progress.echo(timing.message_hms + " elapsed time") }) }