src/Pure/Tools/build_cluster.scala

--- a/src/Pure/Tools/build_cluster.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -262,7 +262,7 @@
       _sessions
     }
     else {
-      for (Exn.Res(session) <- attempts) session.close()
+      for (case Exn.Res(session) <- attempts) session.close()
       error("Failed to connect build cluster")
     }
   }