tuned message;
authorwenzelm
Fri, 27 Jan 2023 16:18:36 +0100
changeset 77111 aa359010d264
parent 77110 595358b9f61d
child 77112 6f2ddbff972c
tuned message;
src/Pure/General/value.scala
--- a/src/Pure/General/value.scala	Fri Jan 27 15:43:45 2023 +0100
+++ b/src/Pure/General/value.scala	Fri Jan 27 16:18:36 2023 +0100
@@ -45,7 +45,7 @@
       try { Some(java.lang.Long.parseLong(s)) }
       catch { case _: NumberFormatException => None }
     def parse(s: java.lang.String): scala.Long =
-      unapply(s) getOrElse error("Bad integer: " + quote(s))
+      unapply(s) getOrElse error("Bad long integer: " + quote(s))
   }
 
   object Double {