# HG changeset patch
# User wenzelm
# Date 1699355210 -3600
# Node ID 65acbafc70e524fe7805c309b2510425cc5ee635
# Parent  f38153e58f21575519ae4424b793f84f2d52a24a
tuned;

diff -r f38153e58f21 -r 65acbafc70e5 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) {