| changeset 74094 | 6113f1db4342 |
| parent 73133 | 497e11537d48 |
| child 75393 | 87ebf5a50283 |
--- a/src/Pure/General/uuid.scala Sat Jul 31 12:48:01 2021 +0200 +++ b/src/Pure/General/uuid.scala Sat Jul 31 15:44:11 2021 +0200 @@ -12,7 +12,6 @@ type T = java.util.UUID def random(): T = java.util.UUID.randomUUID() - def random_string(): String = random().toString def unapply(s: String): Option[T] = try { Some(java.util.UUID.fromString(s)) }