--- a/src/Pure/Tools/dump.scala Tue Mar 24 13:43:29 2020 +0100
+++ b/src/Pure/Tools/dump.scala Wed Mar 25 17:33:46 2020 +0100
@@ -481,6 +481,10 @@
val progress = new Console_Progress(verbose = verbose)
+ val start_date = Date.now()
+
+ if (verbose) progress.echo("Started at " + Build_Log.print_date(start_date))
+
progress.interrupt_handler {
dump(options, logic,
aspects = aspects,
@@ -497,5 +501,11 @@
session_groups = session_groups,
sessions = sessions))
}
+
+ 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(timing.message_hms + " elapsed time")
})
}