src/Pure/Tools/build_process.scala
changeset 77551 ae6df8a8685a
parent 77546 9b9179cda155
child 77552 080422b3d914
equal deleted inserted replaced
77550:ed2f53e1552c 77551:ae6df8a8685a
   833       state
   833       state
   834         .remove_pending(session_name)
   834         .remove_pending(session_name)
   835         .make_result(session_name, Process_Result.undefined, output_shasum)
   835         .make_result(session_name, Process_Result.undefined, output_shasum)
   836     }
   836     }
   837     else {
   837     else {
   838       progress.echo((if (store_heap) "Building " else "Running ") + session_name + " ...")
       
   839 
       
   840       store.init_output(session_name)
       
   841 
       
   842       val (numa_node, state1) = state.numa_next_node(build_context.numa_nodes)
   838       val (numa_node, state1) = state.numa_next_node(build_context.numa_nodes)
   843       val node_info = Host.Node_Info(build_context.hostname, numa_node)
   839       val node_info = Host.Node_Info(build_context.hostname, numa_node)
       
   840 
       
   841       progress.echo(
       
   842         (if (store_heap) "Building " else "Running ") + session_name +
       
   843           if_proper(node_info.numa_node, " on " + node_info) + " ...")
       
   844 
       
   845       store.init_output(session_name)
       
   846 
   844       val job =
   847       val job =
   845         Build_Job.start_session(build_context, progress, log,
   848         Build_Job.start_session(build_context, progress, log,
   846           build_deps.background(session_name), input_shasum, node_info)
   849           build_deps.background(session_name), input_shasum, node_info)
   847       state1.add_running(session_name, job)
   850       state1.add_running(session_name, job)
   848     }
   851     }