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