# HG changeset patch
# User wenzelm
# Date 1708078543 -3600
# Node ID e349a274a9328e3c6c212863b407b6eb77c79dd0
# Parent  0f01c575ff3ef037d5c961a1fc269b8270d4e9e3
more robust: always close, despite failure;

diff -r 0f01c575ff3e -r e349a274a932 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Fri Feb 16 11:12:42 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Fri Feb 16 11:15:43 2024 +0100
@@ -1314,8 +1314,7 @@
       val hosts_current =
         cluster_hosts.forall(host => isabelle.Host.read_info(host_database, host.name).isDefined)
       if (!hosts_current) {
-        Build_Cluster.make(build_context, progress = progress)
-          .open().init().benchmark().close()
+        using(Build_Cluster.make(build_context, progress = progress).open())(_.init().benchmark())
       }
 
       val host_infos = Host_Infos.load(cluster_hosts, host_database)