# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1699003281 -3600
# Node ID 6996a20a1b7c808890e47b7ffa57aa124c698bd8
# Parent  b82c2f801f2c5de21b2819bc3291c98dd3db5197
proper benchmark command;

diff -r b82c2f801f2c -r 6996a20a1b7c src/Pure/System/benchmark.scala
--- a/src/Pure/System/benchmark.scala	Fri Nov 03 10:13:41 2023 +0100
+++ b/src/Pure/System/benchmark.scala	Fri Nov 03 10:21:21 2023 +0100
@@ -16,8 +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 +
-      " " + Bash.string(host.name)
+      options.map(opt => " -o " + Bash.string(opt.print)).mkString
   }
 
   def benchmark(options: Options, progress: Progress = new Progress()): Unit = {