equal
deleted
inserted
replaced
206 Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"), |
206 Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"), |
207 // workaround for jdk-8u102 |
207 // workaround for jdk-8u102 |
208 s => Word.implode(Word.explode(s).map({ |
208 s => Word.implode(Word.explode(s).map({ |
209 case "CET" | "MET" => "GMT+1" |
209 case "CET" | "MET" => "GMT+1" |
210 case "CEST" | "MEST" => "GMT+2" |
210 case "CEST" | "MEST" => "GMT+2" |
|
211 case "EST" => "GMT+1" // FIXME ?? |
211 case a => a }))) |
212 case a => a }))) |
212 |
213 |
213 object Strict_Date |
214 object Strict_Date |
214 { |
215 { |
215 def unapply(s: String): Some[Date] = Some(Date_Format.parse(s)) |
216 def unapply(s: String): Some[Date] = Some(Date_Format.parse(s)) |