# HG changeset patch
# User wenzelm
# Date 1476172204 -7200
# Node ID 96d3988711244aa17cb2680f611b0d98e04d9014
# Parent  387c811cad6a5d052990232f0592561612a15bff
modernized date format;

diff -r 387c811cad6a -r 96d398871124 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Oct 11 09:41:07 2016 +0200
+++ b/src/Pure/Tools/build.scala	Tue Oct 11 09:50:04 2016 +0200
@@ -752,15 +752,15 @@
 
     val progress = new Console_Progress(verbose = verbose)
 
+    val start_date = Date.now()
+
     if (verbose) {
       progress.echo(
-        Library.trim_line(
-          Isabelle_System.bash(
-            """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
+        "Started at " + Build_Log.Log_File.Date_Format(start_date) +
+          " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
       progress.echo(Build_Log.Settings.show() + "\n")
     }
 
-    val start_time = Time.now()
     val results =
       progress.interrupt_handler {
         build(options, progress,
@@ -781,12 +781,11 @@
           session_groups = session_groups,
           sessions = sessions)
       }
-    val elapsed_time = Time.now() - start_time
+    val end_date = Date.now()
+    val elapsed_time = end_date.time - start_date.time
 
     if (verbose) {
-      progress.echo("\n" +
-        Library.trim_line(
-          Isabelle_System.bash("""echo -n "Finished at "; date""").out))
+      progress.echo("\nFinished at " + Build_Log.Log_File.Date_Format(end_date))
     }
 
     val total_timing =