src/Pure/Tools/build_job.scala
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