# HG changeset patch
# User wenzelm
# Date 1476217487 -7200
# Node ID 01716e3c3e68b8ea5c6a37d4bb54de622206e3df
# Parent  646c4d6a6a02435a052b26e3ee86bb2d51acf9ac
tuned message -- more parsable;

diff -r 646c4d6a6a02 -r 01716e3c3e68 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 22:24:14 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 22:24:47 2016 +0200
@@ -42,7 +42,7 @@
 
     def log(date: Date, msg: String)
     {
-      val text = "[" + Build_Log.print_date(date) + " " + hostname + "]: " + msg
+      val text = "[" + Build_Log.print_date(date) + ", " + hostname + "]: " + msg
       File.append(main_log, text + "\n")
       progress.echo(text)
     }