# HG changeset patch # User wenzelm # Date 1709978248 -3600 # Node ID fb4eb78163ae51170577e4e2ac3616798b430020 # Parent 1734334d3dd40838f1e91f41e86d7bd658bb15c7 tuned; diff -r 1734334d3dd4 -r fb4eb78163ae src/Pure/Build/build_process.scala --- a/src/Pure/Build/build_process.scala Sat Mar 09 10:49:12 2024 +0100 +++ b/src/Pure/Build/build_process.scala Sat Mar 09 10:57:28 2024 +0100 @@ -1071,15 +1071,14 @@ ")") + " ...") val session = state.sessions(session_name) + val background = build_deps.background(session_name) val build = Build_Job.start_session(build_context, session, progress, log, server, - build_deps.background(session_name), sources_shasum, input_shasum, node_info, store_heap) + background, sources_shasum, input_shasum, node_info, store_heap) - val job = - Build_Process.Job(session_name, worker_uuid, build_uuid, node_info, start, Some(build)) - - state.add_running(job) + state.add_running( + Build_Process.Job(session_name, worker_uuid, build_uuid, node_info, start, Some(build))) } }