--- a/src/Pure/Tools/dump.scala Sat Mar 04 22:29:21 2023 +0100
+++ b/src/Pure/Tools/dump.scala Sat Mar 04 23:25:30 2023 +0100
@@ -464,7 +464,7 @@
val start_date = Date.now()
- progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date))
+ progress.echo("Started at " + Build_Log.print_date(start_date), verbose = true)
progress.interrupt_handler {
dump(options, logic,
@@ -486,7 +486,7 @@
val end_date = Date.now()
val timing = end_date.time - start_date.time
- progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date))
+ progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true)
progress.echo(timing.message_hms + " elapsed time")
})
}