--- a/src/Pure/Tools/build_job.scala Mon Jun 26 12:07:28 2023 +0200
+++ b/src/Pure/Tools/build_job.scala Mon Jun 26 13:01:58 2023 +0200
@@ -454,7 +454,8 @@
if (process_result.ok && store_heap && heap.is_file) {
val slice = Space.MiB(options.real("build_database_slice")).bytes
val digest =
- using_optional(store.maybe_open_heaps_database())(ML_Heap.store(_, heap, slice))
+ using_optional(store.maybe_open_heaps_database())(
+ ML_Heap.store(_, session_name, heap, slice))
SHA1.shasum(digest, session_name)
}
else SHA1.no_shasum