# HG changeset patch
# User wenzelm
# Date 1693750798 -7200
# Node ID 28a2c55648d502c68106b128233ed3b596e884ff
# Parent  9a5d86549719bb731a3a66d8147f4f959f3c9507
prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;

diff -r 9a5d86549719 -r 28a2c55648d5 src/Pure/Tools/build_cluster.scala
--- 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
     }