prefer local timezone;
authorwenzelm
Sat Oct 08 17:29:42 2016 +0200 (2016-10-08)
changeset 64111b2290b9d0175
parent 64110 c0b96b34c7b9
child 64112 84c1ae86b9af
prefer local timezone;
src/Pure/General/date.scala
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/General/date.scala	Sat Oct 08 17:22:52 2016 +0200
     1.2 +++ b/src/Pure/General/date.scala	Sat Oct 08 17:29:42 2016 +0200
     1.3 @@ -85,6 +85,9 @@
     1.4  
     1.5  sealed case class Date(rep: ZonedDateTime)
     1.6  {
     1.7 +  def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
     1.8 +  def to_utc: Date = to(ZoneId.of("UTC"))
     1.9 +
    1.10    def time: Time = Time.instant(Instant.from(rep))
    1.11    def timezone: ZoneId = rep.getZone
    1.12  
     2.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 17:22:52 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 17:29:42 2016 +0200
     2.3 @@ -311,7 +311,7 @@
     2.4           log_file.lines.last.startsWith(Jenkins.FINISHED) =>
     2.5          log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
     2.6            case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
     2.7 -            parse(Jenkins.engine, "", start, Jenkins.No_End,
     2.8 +            parse(Jenkins.engine, "", start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
     2.9                Jenkins.Isabelle_Version, Jenkins.AFP_Version)
    2.10            case _ => Meta_Info.empty
    2.11          }