# HG changeset patch
# User wenzelm
# Date 1475940582 -7200
# Node ID b2290b9d017519a1aedae139454f2717c2149067
# Parent  c0b96b34c7b9f55cb047687cd778e55bc60f5734
prefer local timezone;

diff -r c0b96b34c7b9 -r b2290b9d0175 src/Pure/General/date.scala
--- 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
 
diff -r c0b96b34c7b9 -r b2290b9d0175 src/Pure/Tools/build_log.scala
--- 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
         }