src/Pure/Admin/build_log.scala
changeset 69980 f2e3adfd916f
parent 69299 2fd070377c99
     1.1 --- a/src/Pure/Admin/build_log.scala	Mon Mar 25 16:11:28 2019 +0100
     1.2 +++ b/src/Pure/Admin/build_log.scala	Mon Mar 25 16:45:08 2019 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  
     1.5  
     1.6  import java.io.{File => JFile}
     1.7 -import java.time.ZoneId
     1.8  import java.time.format.{DateTimeFormatter, DateTimeParseException}
     1.9  import java.util.Locale
    1.10  
    1.11 @@ -157,7 +156,7 @@
    1.12            List(Locale.ENGLISH, Locale.GERMAN)) :::
    1.13          List(
    1.14            DateTimeFormatter.RFC_1123_DATE_TIME,
    1.15 -          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
    1.16 +          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(Date.timezone_berlin))
    1.17  
    1.18        def tune_timezone(s: String): String =
    1.19          s match {
    1.20 @@ -429,7 +428,7 @@
    1.21                log_file.lines.takeWhile(_ != Jenkins.CONFIGURATION).collectFirst({
    1.22                  case Jenkins.Host(a, b) => a + "." + b
    1.23                }).getOrElse("")
    1.24 -            parse(Jenkins.engine, host, start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
    1.25 +            parse(Jenkins.engine, host, start.to(Date.timezone_berlin), Jenkins.No_End,
    1.26                Jenkins.Isabelle_Version, Jenkins.AFP_Version)
    1.27            case _ => Meta_Info.empty
    1.28          }