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 {