detect host name;
authorwenzelm
Mon, 01 May 2017 11:33:06 +0200
changeset 65663 61cd86bb9613
parent 65662 3db6a13fdffd
child 65664 c84db5e0dd6d
detect host name;
src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon May 01 11:24:41 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 01 11:33:06 2017 +0200
@@ -342,6 +342,7 @@
   object Jenkins
   {
     val engine = "jenkins"
+    val Host = new Regex("""^Building remotely on (\S+) \((\S+)\).*$""")
     val Start = new Regex("""^Started .*$""")
     val Start_Date = new Regex("""^Build started at (.+)$""")
     val No_End = new Regex("""$.""")
@@ -409,7 +410,11 @@
          log_file.lines.last.startsWith(Jenkins.FINISHED) =>
         log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
           case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
-            parse(Jenkins.engine, "", start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
+            val host =
+              log_file.lines.takeWhile(_ != Jenkins.CONFIGURATION).collectFirst({
+                case Jenkins.Host(a, b) => a + "." + b
+              }).getOrElse("")
+            parse(Jenkins.engine, host, start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
               Jenkins.Isabelle_Version, Jenkins.AFP_Version)
           case _ => Meta_Info.empty
         }