acceptedgood first issue
倉庫指標
- 星標
- (1,882 顆星)
- PR 合併指標
- (平均合併 1天 20小時) (30 天內合併 345 個 PR)
描述
I'd like to set the dune build directory from the dune-workspace file instead of specifying it on the command line. It looked like I might be able to achieve this by using the (env) stanza to set the DUNE_BUILD_DIR environment variable.
I tried (env (_ (env-vars (DUNE_BUILD_DIR /path/to/new/_build)))) but that din't seem to have any effect (the _build directory in the root was still generated). I also confirmed that setting the environment variable normally on the command line does produce the expected result.
Incidentally this seems like a pretty circuitous way to set this setting - it should probably be configurable from the dune-workspace file natively.