--- a/src/Pure/System/options.scala Tue Aug 22 09:28:44 2023 +0200
+++ b/src/Pure/System/options.scala Tue Aug 22 09:39:37 2023 +0200
@@ -83,8 +83,6 @@
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 {
@@ -304,6 +302,9 @@
def description(name: String): String = check_name(name).description
+ def spec(name: String): Options.Spec =
+ Options.Spec(name, Some(check_name(name).value))
+
/* check */
--- a/src/Pure/Tools/build_cluster.scala Tue Aug 22 09:28:44 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala Tue Aug 22 09:39:37 2023 +0200
@@ -159,7 +159,7 @@
val script =
Build.build_worker_command(host,
ssh = ssh,
- build_options = List(options.check_name("build_database_server").spec),
+ build_options = List(options.spec("build_database_server")),
build_id = build_context.build_uuid,
isabelle_home = remote_isabelle_home,
afp_root = remote_afp_root)