# HG changeset patch
# User wenzelm
# Date 1699444824 -3600
# Node ID 90756ad4d8d7963dce9168ffc07d439164c6ecf4
# Parent  715f1bd2199363fbbd7d83cce29c76d76e4bbbc1
more accurate treatment of surrounding whitespace;

diff -r 715f1bd21993 -r 90756ad4d8d7 src/Pure/System/benchmark.scala
--- a/src/Pure/System/benchmark.scala	Wed Nov 08 12:41:41 2023 +0100
+++ b/src/Pure/System/benchmark.scala	Wed Nov 08 13:00:24 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.Spec.bash_strings(options)
+      Options.Spec.bash_strings(options, bg = true)
   }
 
   def benchmark(options: Options, progress: Progress = new Progress()): Unit = {
diff -r 715f1bd21993 -r 90756ad4d8d7 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Nov 08 12:41:41 2023 +0100
+++ b/src/Pure/System/options.scala	Wed Nov 08 13:00:24 2023 +0100
@@ -41,8 +41,14 @@
 
     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(" ", " ", " ")
+    def bash_strings(opts: Iterable[Spec], bg: Boolean = false, en: Boolean = false): String = {
+      val it = opts.iterator
+      if (it.isEmpty) ""
+      else {
+        it.map(opt => "-o " + Bash.string(opt.toString))
+          .mkString(if (bg) " " else "", " ", if (en) " " else "")
+      }
+    }
   }
 
   sealed case class Spec(name: String, value: Option[String] = None, permissive: Boolean = false) {
diff -r 715f1bd21993 -r 90756ad4d8d7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Nov 08 12:41:41 2023 +0100
+++ b/src/Pure/Tools/build.scala	Wed Nov 08 13:00:24 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.Spec.bash_strings(options) +
+      Options.Spec.bash_strings(options, bg = true) +
       if_proper(quiet, " -q") +
       if_proper(verbose, " -v")
   }