src/Pure/System/options.scala
changeset 78556 20360824863a
parent 78407 b262ecc98319
child 78559 020fecb4da0c
--- a/src/Pure/System/options.scala	Mon Aug 21 15:28:35 2023 +0200
+++ b/src/Pure/System/options.scala	Mon Aug 21 15:54:08 2023 +0200
@@ -83,6 +83,8 @@
     description: String,
     section: String
   ) {
+    def spec: Spec = Spec(name, Some(value))
+
     private def print_value(x: String): String = if (typ == Options.String) quote(x) else x
     private def print_standard: String =
       standard_value match {