prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;
--- a/src/Pure/Tools/build_cluster.scala Sun Sep 03 16:18:06 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala Sun Sep 03 16:19:58 2023 +0200
@@ -171,7 +171,8 @@
build_id = build_context.build_uuid,
isabelle_home = remote_isabelle_home,
afp_root = remote_afp_root,
- dirs = Path.split(host.dirs).map(remote_isabelle.expand_path))
+ dirs = Path.split(host.dirs).map(remote_isabelle.expand_path),
+ quiet = true)
remote_isabelle.bash(script).check
}