changeset 73715 | bf51c23f3f99 |
parent 73712 | 3eba8d4b624b |
child 75393 | 87ebf5a50283 |
--- a/src/Pure/General/properties.scala Mon May 17 14:07:13 2021 +0200 +++ b/src/Pure/General/properties.scala Mon May 17 14:07:51 2021 +0200 @@ -16,7 +16,8 @@ object Eq { - def apply(entry: Entry): java.lang.String = entry._1 + "=" + entry._2 + def apply(a: java.lang.String, b: java.lang.String): java.lang.String = a + "=" + b + def apply(entry: Entry): java.lang.String = apply(entry._1, entry._2) def unapply(str: java.lang.String): Option[Entry] = {