diff -r d3de24c50b08 -r 6a078c80eab6 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Sun Jan 15 20:00:44 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Sun Jan 15 20:20:59 2023 +0100 @@ -592,7 +592,7 @@ val heap_digest = if (result2.ok && do_store && store.output_heap(session_name).is_file) - Some(Sessions.write_heap_digest(store.output_heap(session_name))) + Some(ML_Heap.write_digest(store.output_heap(session_name))) else None (result2, heap_digest)