# HG changeset patch
# User wenzelm
# Date 1476386629 -7200
# Node ID c43dedbb81181a3072ab2bd8b707387e9132a01e
# Parent  6688b9cd443b7127ea88ee372a77730a13235a68
tuned message;

diff -r 6688b9cd443b -r c43dedbb8118 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 21:16:42 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 21:23:49 2016 +0200
@@ -121,7 +121,7 @@
       val elapsed_time = end_date.time - start_date.time
       val msg =
         (if (err.isEmpty) "finished" else "ERROR " + err.get) +
-        (if (elapsed_time.seconds < 3.0) "" else ", elapsed time " + elapsed_time.message_hms)
+        (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)")
       log(end_date, msg)
     }