src/Pure/Build/build_process.scala
changeset 82720 956ecf2c07a0
parent 82142 508a673c87ac
child 82752 20ffc02d0b0e
equal deleted inserted replaced
82719:2d99f3e24da4 82720:956ecf2c07a0
  1159     state: Build_Process.State,
  1159     state: Build_Process.State,
  1160     session_name: String,
  1160     session_name: String,
  1161     ancestor_results: List[Build_Process.Result]
  1161     ancestor_results: List[Build_Process.Result]
  1162   ): Build_Process.State = {
  1162   ): Build_Process.State = {
  1163     val sources_shasum = state.sessions(session_name).sources_shasum
  1163     val sources_shasum = state.sessions(session_name).sources_shasum
  1164     val input_shasum = ML_Process.make_shasum(ancestor_results.map(_.output_shasum))
  1164     val input_shasum = ML_Process.make_shasum(store, ancestor_results.map(_.output_shasum))
  1165     val store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
  1165     val store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
  1166     val (current, output_shasum) =
  1166     val (current, output_shasum) =
  1167       store.check_output(_database_server, session_name,
  1167       store.check_output(_database_server, session_name,
  1168         sources_shasum = sources_shasum,
  1168         sources_shasum = sources_shasum,
  1169         input_shasum = input_shasum,
  1169         input_shasum = input_shasum,