src/Pure/Tools/build_cluster.scala

--- a/src/Pure/Tools/build_cluster.scala	Sun Sep 03 18:09:00 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Sun Sep 03 19:28:59 2023 +0200
@@ -263,7 +263,7 @@
       _sessions
     }
     else {
-      for (Exn.Res(session) <- attempts) session.close()
+      for (case Exn.Res(session) <- attempts) session.close()
       error("Failed to connect build cluster")
     }
   }