--- 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
}