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 }