# HG changeset patch
# User wenzelm
# Date 1674832716 -3600
# Node ID aa359010d264895d60a357ee8f89b64f0ec6b833
# Parent  595358b9f61d25af5075b6cf816affe2ee39e471
tuned message;

diff -r 595358b9f61d -r aa359010d264 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 {