src/Pure/General/date.scala
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)