# HG changeset patch
# User wenzelm
# Date 1585154026 -3600
# Node ID 6db526adccacf943f28c302fe4f3772b56aa89bd
# Parent  4269db8981b8d09dbfb1382858787e80908a555d
clarified messages: indicate termination explicitly;

diff -r 4269db8981b8 -r 6db526adccac src/Pure/Tools/dump.scala
--- 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")
     })
 }