| changeset 78638 | 28a2c55648d5 |
| parent 78584 | 92ef737f412c |
| child 78639 | ca56952b7322 |
--- 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 }