author | wenzelm |
Wed, 19 Jul 2023 11:31:19 +0200 | |
changeset 78403 | a09929ad05b6 |
parent 78402 | e25f1d343fa7 |
child 78404 | b66b6cc1eb8c |
--- 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 =>