# HG changeset patch
# User wenzelm
# Date 1699354954 -3600
# Node ID f38153e58f21575519ae4424b793f84f2d52a24a
# Parent  89274adb0ebe63f58dd97b432670b64a6c8bc035
proper Option.Spec.toString for bash script: avoid Token.quote_name of Options.Spec.print_value (amending 3d1746a716fa, see also 39f6f180008d);

diff -r 89274adb0ebe -r f38153e58f21 src/Pure/System/benchmark.scala
--- a/src/Pure/System/benchmark.scala	Sun Nov 05 19:55:18 2023 +0100
+++ b/src/Pure/System/benchmark.scala	Tue Nov 07 12:02:34 2023 +0100
@@ -16,7 +16,7 @@
   ): String = {
     val options = Options.Spec("build_hostname", Some(host.name)) :: host.options
     ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " benchmark" +
-      options.map(opt => " -o " + Bash.string(opt.print)).mkString
+      Options.Spec.bash_strings(options)
   }
 
   def benchmark(options: Options, progress: Progress = new Progress()): Unit = {
diff -r 89274adb0ebe -r f38153e58f21 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sun Nov 05 19:55:18 2023 +0100
+++ b/src/Pure/System/options.scala	Tue Nov 07 12:02:34 2023 +0100
@@ -29,6 +29,9 @@
       }
 
     def print(name: String, value: String): String = Properties.Eq(name, print_value(value))
+
+    def bash_strings(opts: Iterable[Spec]): String =
+      opts.iterator.map(opt => "-o " + Bash.string(opt.toString)).mkString(" ", " ", " ")
   }
 
   sealed case class Spec(name: String, value: Option[String] = None, permissive: Boolean = false) {
diff -r 89274adb0ebe -r f38153e58f21 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Nov 05 19:55:18 2023 +0100
+++ b/src/Pure/Tools/build.scala	Tue Nov 07 12:02:34 2023 +0100
@@ -589,7 +589,7 @@
       if_proper(afp_root, " -A " + ssh.bash_path(afp_root.get)) +
       dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
       if_proper(host.numa, " -N") + " -j" + host.jobs +
-      options.map(opt => " -o " + Bash.string(opt.print)).mkString +
+      Options.Spec.bash_strings(options) +
       if_proper(quiet, " -q") +
       if_proper(verbose, " -v")
   }