tuned message -- more parsable;
authorwenzelm
Tue Oct 11 22:24:47 2016 +0200 (2016-10-11)
changeset 6415601716e3c3e68
parent 64155 646c4d6a6a02
child 64157 3e4400f21310
tuned message -- more parsable;
src/Pure/Admin/isabelle_cronjob.scala
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 22:24:14 2016 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 22:24:47 2016 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5      def log(date: Date, msg: String)
     1.6      {
     1.7 -      val text = "[" + Build_Log.print_date(date) + " " + hostname + "]: " + msg
     1.8 +      val text = "[" + Build_Log.print_date(date) + ", " + hostname + "]: " + msg
     1.9        File.append(main_log, text + "\n")
    1.10        progress.echo(text)
    1.11      }