# HG changeset patch # User wenzelm # Date 1699005315 -3600 # Node ID 88eb92a52f9bbfae5e87472722f907b58561cedf # Parent 6996a20a1b7c808890e47b7ffa57aa124c698bd8# Parent 95bbf9a576b38611d32016fe07797ab55c646bfe merged diff -r 95bbf9a576b3 -r 88eb92a52f9b src/Pure/System/benchmark.scala --- a/src/Pure/System/benchmark.scala Fri Nov 03 10:30:51 2023 +0100 +++ b/src/Pure/System/benchmark.scala Fri Nov 03 10:55:15 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 = {