| changeset 79620 | 3914bca631b9 |
| parent 79619 | 50ec6a68d36f |
| child 79626 | 73b8ac4b0492 |
--- a/src/Pure/Build/build_cluster.scala Thu Feb 15 12:42:00 2024 +0100 +++ b/src/Pure/Build/build_cluster.scala Thu Feb 15 12:48:25 2024 +0100 @@ -185,7 +185,7 @@ def benchmark(): Unit = { val script = - Benchmark.benchmark_command(host, ssh = ssh, isabelle_home = remote_isabelle_home) + Build_Benchmark.benchmark_command(host, ssh = ssh, isabelle_home = remote_isabelle_home) remote_isabelle.bash(script).check }