src/Pure/Build/store.scala
changeset 79677 49370f0f7911
parent 79676 0cac7e3634d0
child 79682 1fa1b32b0379
--- a/src/Pure/Build/store.scala	Mon Feb 19 11:30:37 2024 +0100
+++ b/src/Pure/Build/store.scala	Mon Feb 19 11:39:15 2024 +0100
@@ -308,7 +308,7 @@
     def get_database: Option[SHA1.Digest] = {
       for {
         db <- database_server
-        digest <- ML_Heap.get_entries(db, List(name)).valuesIterator.nextOption()
+        digest <- ML_Heap.read_digests(db, List(name)).valuesIterator.nextOption()
       } yield digest
     }