src/Pure/Tools/build_process.scala
changeset 78359 cb0a90df4871
parent 78356 974dbe256a37
child 78364 e33cca11b474
equal deleted inserted replaced
78358:f5cf8e500dee 78359:cb0a90df4871
  1013 
  1013 
  1014       progress.echo(
  1014       progress.echo(
  1015         (if (store_heap) "Building " else "Running ") + session_name +
  1015         (if (store_heap) "Building " else "Running ") + session_name +
  1016           if_proper(node_info.numa_node, " on " + node_info) + " ...")
  1016           if_proper(node_info.numa_node, " on " + node_info) + " ...")
  1017 
  1017 
  1018       store.clean_output(_database_server, session_name, session_init = true)
       
  1019 
       
  1020       val session = state.sessions(session_name)
  1018       val session = state.sessions(session_name)
  1021 
  1019 
  1022       val build =
  1020       val build =
  1023         Build_Job.start_session(build_context, session, progress, log, _database_server,
  1021         Build_Job.start_session(build_context, session, progress, log, _database_server,
  1024           build_deps.background(session_name), sources_shasum, input_shasum, node_info, store_heap)
  1022           build_deps.background(session_name), sources_shasum, input_shasum, node_info, store_heap)