# HG changeset patch
# User wenzelm
# Date 1687355808 -7200
# Node ID 752a7751b3d32274428bc7c105644329205b0612
# Parent  6e52cda26ad4e51c2a963a3be54ba636305c3e73
more robust try-finally;

diff -r 6e52cda26ad4 -r 752a7751b3d3 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Jun 21 15:53:38 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Wed Jun 21 15:56:48 2023 +0200
@@ -452,11 +452,12 @@
         val output_shasum = {
           val heap = store.output_heap(session_name)
           if (process_result.ok && store_heap && heap.is_file) {
-            val database = store.maybe_open_heaps_database()
             val slice = Space.MiB(options.real("build_database_slice")).bytes
-            val digest =
+            val digest = {
+              val database = store.maybe_open_heaps_database()
               try { ML_Heap.store(database, heap, slice = slice) }
               finally { database.foreach(_.close()) }
+            }
             SHA1.shasum(digest, session_name)
           }
           else SHA1.no_shasum