src/Pure/Tools/build_cluster.scala
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
     }