# HG changeset patch
# User wenzelm
# Date 1689759079 -7200
# Node ID a09929ad05b64416aef812f5df49b1ea36208dc4
# Parent  e25f1d343fa7f51d86a2f0242adca57f40a03683
proper build_options (amending 822ddccda899);

diff -r e25f1d343fa7 -r a09929ad05b6 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Jul 19 10:56:19 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jul 19 11:31:19 2023 +0200
@@ -137,7 +137,7 @@
   ): Results = {
     val build_engine = Engine(engine_name(options))
 
-    val store = build_engine.build_store(options, cache = cache)
+    val store = build_engine.build_store(options, build_hosts = build_hosts, cache = cache)
     val build_options = store.options
 
     using(store.open_server()) { server =>