src/Pure/System/options.scala
changeset 73712 3eba8d4b624b
parent 73359 d8a0e996614b
child 73715 bf51c23f3f99
--- a/src/Pure/System/options.scala	Mon May 17 13:37:47 2021 +0200
+++ b/src/Pure/System/options.scala	Mon May 17 13:40:01 2021 +0200
@@ -355,12 +355,10 @@
   }
 
   def + (str: String): Options =
-  {
-    str.indexOf('=') match {
-      case -1 => this + (str, None)
-      case i => this + (str.substring(0, i), str.substring(i + 1))
+    str match {
+      case Properties.Eq((a, b)) => this + (a, b)
+      case _ => this + (str, None)
     }
-  }
 
   def ++ (specs: List[Options.Spec]): Options =
     specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) }