# HG changeset patch
# User wenzelm
# Date 1493631186 -7200
# Node ID 61cd86bb9613f4d72475b961cc6c10fa6749d0cd
# Parent  3db6a13fdffdad186ecbd6468d8c7bc958dc664e
detect host name;

diff -r 3db6a13fdffd -r 61cd86bb9613 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
         }