src/Pure/Build/build_process.scala
changeset 82752 20ffc02d0b0e
parent 82720 956ecf2c07a0
equal deleted inserted replaced
82751:84534cc9c97e 82752:20ffc02d0b0e
  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(store, ancestor_results.map(_.output_shasum))
  1164     val input_shasum = store.make_shasum(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,