--- a/src/Pure/General/date.scala Sat Oct 08 17:22:52 2016 +0200
+++ b/src/Pure/General/date.scala Sat Oct 08 17:29:42 2016 +0200
@@ -85,6 +85,9 @@
sealed case class Date(rep: ZonedDateTime)
{
+ def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
+ def to_utc: Date = to(ZoneId.of("UTC"))
+
def time: Time = Time.instant(Instant.from(rep))
def timezone: ZoneId = rep.getZone
--- a/src/Pure/Tools/build_log.scala Sat Oct 08 17:22:52 2016 +0200
+++ b/src/Pure/Tools/build_log.scala Sat Oct 08 17:29:42 2016 +0200
@@ -311,7 +311,7 @@
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, Jenkins.No_End,
+ parse(Jenkins.engine, "", start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
Jenkins.Isabelle_Version, Jenkins.AFP_Version)
case _ => Meta_Info.empty
}