--- a/src/Pure/Tools/build_cluster.scala Mon Aug 21 20:40:15 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala Tue Aug 22 09:28:44 2023 +0200
@@ -157,10 +157,9 @@
def start(): Process_Result = {
val script =
- Build.build_worker_command(
- List(options.check_name("build_database_server").spec),
- host,
+ Build.build_worker_command(host,
ssh = ssh,
+ build_options = List(options.check_name("build_database_server").spec),
build_id = build_context.build_uuid,
isabelle_home = remote_isabelle_home,
afp_root = remote_afp_root)