diff -r 84534cc9c97e -r 20ffc02d0b0e src/Pure/Build/build_schedule.scala --- a/src/Pure/Build/build_schedule.scala Tue Jun 24 21:58:20 2025 +0200 +++ b/src/Pure/Build/build_schedule.scala Tue Jun 24 22:08:20 2025 +0200 @@ -1132,7 +1132,7 @@ store.check_output( _database_server, session_name, sources_shasum = state.sessions(session_name).sources_shasum, - input_shasum = ML_Process.make_shasum(store, ancestor_results.map(_.output_shasum)), + input_shasum = store.make_shasum(ancestor_results.map(_.output_shasum)), build_thorough = build_context.sessions_structure(session_name).build_thorough, fresh_build = build_context.fresh_build, store_heap = build_context.store_heap || state.sessions.store_heap(session_name))._1