# HG changeset patch
# User wenzelm
# Date 1475856430 -7200
# Node ID 210aabe359ab9c4ccdfda4403d5e8a36771b1955
# Parent  a77c57235bae30f12fdd91c6614314616240d387
more permissive for old logs;

diff -r a77c57235bae -r 210aabe359ab src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 17:46:36 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 18:07:10 2016 +0200
@@ -196,7 +196,7 @@
         // workaround for jdk-8u102
         s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a })))
 
-    val Test_Start = new Regex("""^Start test for .+ at (.+), (\S+)$""")
+    val Test_Start = new Regex("""^Start test (?:for \S+)? at (.+), (\S+)$""")
     val Test_End = new Regex("""^End test on (.+), \S+, elapsed time:.*$""")
     val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
     val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
@@ -209,19 +209,17 @@
         (start, log_file.lines.last) match {
           case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) =>
             val isabelle_version =
-              log_file.find_match(AFP.Isabelle_Version) getOrElse
-                log_file.err("missing Isabelle version")
+              log_file.find_match(AFP.Isabelle_Version).map((Field.isabelle_version, _))
             val afp_version =
-              log_file.find_match(AFP.AFP_Version) getOrElse
-                log_file.err("missing AFP version")
+              log_file.find_match(AFP.AFP_Version).map((Field.afp_version, _))
 
             Header(Header_Kind.AFP_TEST,
               List(
                 Field.build_host -> hostname,
                 Field.build_start -> start_date.toString,
-                Field.build_end -> end_date.toString,
-                Field.isabelle_version -> isabelle_version,
-                Field.afp_version -> afp_version),
+                Field.build_end -> end_date.toString) :::
+              isabelle_version.toList :::
+              afp_version.toList,
               log_file.get_settings(Settings.all_settings))
 
           case _ => log_file.err("cannot detect start/end date in afp-test log")