proper build_options (amending 822ddccda899);
authorwenzelm
Wed, 19 Jul 2023 11:31:19 +0200
changeset 78403 a09929ad05b6
parent 78402 e25f1d343fa7
child 78404 b66b6cc1eb8c
proper build_options (amending 822ddccda899);
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 =>