src/Pure/Tools/build_job.scala
changeset 78842 eb572f7b6689
parent 78674 88f47c70187a
child 78985 24e686fe043e
--- a/src/Pure/Tools/build_job.scala	Wed Oct 18 19:53:39 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Wed Oct 18 20:07:54 2023 +0200
@@ -117,7 +117,7 @@
     private val future_result: Future[Option[Result]] =
       Future.thread("build", uninterruptible = true) {
         val info = session_background.sessions_structure(session_name)
-        val options = build_context.engine.process_options(info.options, node_info)
+        val options = Host.node_options(info.options, node_info)
 
         val store = build_context.store