changeset 78435 | a623cb346b4a |
parent 78428 | 48cbee2a6f2e |
child 78529 | 0e79fa88cab6 |
--- a/src/Pure/Tools/build_job.scala Sat Jul 22 13:31:55 2023 +0200 +++ b/src/Pure/Tools/build_job.scala Sat Jul 22 16:01:46 2023 +0200 @@ -114,7 +114,7 @@ private val future_result: Future[(Process_Result, SHA1.Shasum)] = Future.thread("build", uninterruptible = true) { val info = session_background.sessions_structure(session_name) - val options = node_info.process_policy(info.options) + val options = build_context.engine.process_options(info.options, node_info) val store = build_context.store