# HG changeset patch # User wenzelm # Date 1692689977 -7200 # Node ID 020fecb4da0c4afd632ab5ed1b32e742dbd20ef4 # Parent ca0fe2802123c757a6d0366b6dcc12cf067f4982 tuned signature; diff -r ca0fe2802123 -r 020fecb4da0c src/Pure/System/options.scala --- 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 */ diff -r ca0fe2802123 -r 020fecb4da0c src/Pure/Tools/build_cluster.scala --- 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)