tuned;
authorwenzelm
Tue, 07 Nov 2023 12:06:50 +0100
changeset 78909 65acbafc70e5
parent 78908 f38153e58f21
child 78910 d305af09fbad
tuned;
src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Nov 07 12:02:34 2023 +0100
+++ b/src/Pure/System/options.scala	Tue Nov 07 12:06:50 2023 +0100
@@ -36,7 +36,11 @@
 
   sealed case class Spec(name: String, value: Option[String] = None, permissive: Boolean = false) {
     override def toString: String = name + if_proper(value, "=" + value.get)
-    def print: String = name + if_proper(value, "=" + Spec.print_value(value.get))
+    def print: String =
+      value match {
+        case None => name
+        case Some(v) => Spec.print(name, v)
+      }
   }
 
   sealed case class Change(name: String, value: String, unknown: Boolean) {