# HG changeset patch # User wenzelm # Date 1678127852 -3600 # Node ID ae6df8a8685a7e5a208bb563e7e2dfcf3dea44bc # Parent ed2f53e1552c8f5c509a913d87c1713e7995c2b1 clarified messages; diff -r ed2f53e1552c -r ae6df8a8685a src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Mon Mar 06 19:18:53 2023 +0100 +++ b/src/Pure/Admin/build_log.scala Mon Mar 06 19:37:32 2023 +0100 @@ -443,7 +443,8 @@ new Regex("""^Finished ([^\s/]+) \((\d+):(\d+):(\d+) elapsed time.*$""") val Session_Timing = new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""") - val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""") + val Session_Started1 = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""") + val Session_Started2 = new Regex("""^(?:Running|Building) (\S+) on \S+ \.\.\.$""") val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""") val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""") @@ -486,7 +487,10 @@ chapter += (name -> chapt) groups += (name -> Word.explode(grps)) - case Session_Started(name) => + case Session_Started1(name) => + started += name + + case Session_Started2(name) => started += name case Session_Finished1(name, diff -r ed2f53e1552c -r ae6df8a8685a src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Mon Mar 06 19:18:53 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Mon Mar 06 19:37:32 2023 +0100 @@ -835,12 +835,15 @@ .make_result(session_name, Process_Result.undefined, output_shasum) } else { - progress.echo((if (store_heap) "Building " else "Running ") + session_name + " ...") + val (numa_node, state1) = state.numa_next_node(build_context.numa_nodes) + val node_info = Host.Node_Info(build_context.hostname, numa_node) + + progress.echo( + (if (store_heap) "Building " else "Running ") + session_name + + if_proper(node_info.numa_node, " on " + node_info) + " ...") store.init_output(session_name) - val (numa_node, state1) = state.numa_next_node(build_context.numa_nodes) - val node_info = Host.Node_Info(build_context.hostname, numa_node) val job = Build_Job.start_session(build_context, progress, log, build_deps.background(session_name), input_shasum, node_info)