author | wenzelm |
Sun, 27 Aug 2023 12:57:59 +0200 | |
changeset 78584 | 92ef737f412c |
parent 78583 | 8f11794211ef |
child 78585 | cf114894a5ed |
--- a/src/Pure/Tools/build_cluster.scala Sun Aug 27 12:49:43 2023 +0200 +++ b/src/Pure/Tools/build_cluster.scala Sun Aug 27 12:57:59 2023 +0200 @@ -172,7 +172,7 @@ isabelle_home = remote_isabelle_home, afp_root = remote_afp_root, dirs = Path.split(host.dirs).map(remote_isabelle.expand_path)) - remote_isabelle.bash(script).print.check + remote_isabelle.bash(script).check } override def close(): Unit = ssh.close()