# HG changeset patch
# User wenzelm
# Date 1493636108 -7200
# Node ID 9b7fb07b4a9634e672e14a5d8255f9ba2a61cc83
# Parent  c84db5e0dd6d98084a7f0cc35cea8c1450378871
more robust detection of Jenkins log;

diff -r c84db5e0dd6d -r 9b7fb07b4a96 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon May 01 12:28:33 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 01 12:55:08 2017 +0200
@@ -345,14 +345,13 @@
     val log_prefix = "jenkins_"
     val engine = "jenkins"
     val Host = new Regex("""^Building remotely on (\S+) \((\S+)\).*$""")
-    val Start = new Regex("""^Started .*$""")
+    val Start = new Regex("""^(?:Started by an SCM change|Started from command line by admin|).*$""")
     val Start_Date = new Regex("""^Build started at (.+)$""")
     val No_End = new Regex("""$.""")
     val Isabelle_Version = new Regex("""^Isabelle id (\S+)$""")
     val AFP_Version = new Regex("""^AFP id (\S+)$""")
     val CONFIGURATION = "=== CONFIGURATION ==="
     val BUILD = "=== BUILD ==="
-    val FINISHED = "Finished: "
   }
 
   private def parse_meta_info(log_file: Log_File): Meta_Info =
@@ -407,9 +406,7 @@
         parse(AFP_Test.engine, "", start, AFP_Test.End,
           AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
 
-      case Jenkins.Start() :: _
-      if log_file.lines.contains(Jenkins.CONFIGURATION) ||
-         log_file.lines.last.startsWith(Jenkins.FINISHED) =>
+      case Jenkins.Start() :: _ =>
         log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
           case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
             val host =