proper benchmark command;
authorFabian Huch <huch@in.tum.de>
Fri, 03 Nov 2023 10:21:21 +0100
changeset 78887 6996a20a1b7c
parent 78886 b82c2f801f2c
child 78889 88eb92a52f9b
proper benchmark command;
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 = {