# 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)