src/Pure/Tools/build_log.scala
changeset 64096 5edeb60a7ec5
parent 64095 1a6d37c31df9
child 64098 099518e8af2c
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 22:58:24 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 23:11:20 2016 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import java.util.Locale
     1.8  import java.io.{File => JFile}
     1.9  import java.time.ZonedDateTime
    1.10  import java.time.format.{DateTimeFormatter, DateTimeParseException}
    1.11 @@ -182,7 +183,9 @@
    1.12    /* header and meta data */
    1.13  
    1.14    val Date_Format =
    1.15 -    Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    1.16 +    Date.Format.make_variants(
    1.17 +      List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    1.18 +      List(Locale.ENGLISH, Locale.GERMAN),
    1.19        // workaround for jdk-8u102
    1.20        s => Word.implode(Word.explode(s).map({
    1.21          case "CET" | "MET" => "GMT+1"