more robust try-finally;
authorwenzelm
Wed, 21 Jun 2023 15:56:48 +0200 (20 months ago)
changeset 78192 752a7751b3d3
parent 78191 6e52cda26ad4
child 78193 443a443bbe7b
more robust try-finally;
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