# HG changeset patch
# User wenzelm
# Date 1687355618 -7200
# Node ID 6e52cda26ad4e51c2a963a3be54ba636305c3e73
# Parent  40ae1cd71133be4f7350f830b222b3f83af2e0ba
tuned signature;

diff -r 40ae1cd71133 -r 6e52cda26ad4 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Wed Jun 21 15:41:18 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Wed Jun 21 15:53:38 2023 +0200
@@ -111,7 +111,7 @@
   def clean_entry(db: SQL.Database, name: String): Unit =
     Data.transaction_lock(db, create = true) { Data.clean_entry(db, name) }
 
-  def write_digest(
+  def store(
     database: Option[SQL.Database],
     heap: Path,
     slice: Long,
diff -r 40ae1cd71133 -r 6e52cda26ad4 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)
           }