src/Pure/Tools/build_job.scala

--- a/src/Pure/Tools/build_job.scala	Wed Jun 21 15:41:18 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Wed Jun 21 15:53:38 2023 +0200
@@ -455,7 +455,7 @@
             val database = store.maybe_open_heaps_database()
             val slice = Space.MiB(options.real("build_database_slice")).bytes
             val digest =
-              try { ML_Heap.write_digest(database, heap, slice = slice) }
+              try { ML_Heap.store(database, heap, slice = slice) }
               finally { database.foreach(_.close()) }
             SHA1.shasum(digest, session_name)
           }