diff -r e7deaadc5eab -r bf51c23f3f99 src/Pure/General/properties.scala
--- 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] =
     {