changeset 73120 | c3589f2dff31 |
parent 71601 | 97ccf48c2f0c |
child 73649 | 029de1598940 |
--- a/src/Pure/General/date.scala Sat Jan 09 22:41:08 2021 +0100 +++ b/src/Pure/General/date.scala Sun Jan 10 13:04:29 2021 +0100 @@ -23,7 +23,7 @@ { def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format = { - require(fmts.nonEmpty) + require(fmts.nonEmpty, "no date formats") new Format { def apply(date: Date): String = fmts.head.format(date.rep)