| changeset 78674 | 88f47c70187a |
| parent 78643 | d5a1d64a563d |
| child 78840 | 4b528ca25573 |
--- a/src/Pure/Tools/build_cluster.scala Tue Sep 19 13:46:11 2023 +0200 +++ b/src/Pure/Tools/build_cluster.scala Tue Sep 19 19:48:54 2023 +0200 @@ -258,7 +258,7 @@ capture(host, "open") { host.open_session(build_context, progress = progress) }, remote_hosts, thread = true) - if (attempts.forall(Exn.the_res.isDefinedAt)) { + if (attempts.forall(Exn.is_res)) { _sessions = attempts.map(Exn.the_res) _sessions }