prefer local timezone;
authorwenzelm
Sat, 08 Oct 2016 17:29:42 +0200
changeset 64111 b2290b9d0175
parent 64110 c0b96b34c7b9
child 64112 84c1ae86b9af
prefer local timezone;
src/Pure/General/date.scala
src/Pure/Tools/build_log.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
 
--- 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
         }