acceptedgood first issue
Repository metrics
- Stars
- (1,882 個のスター)
- PR merge metrics
- (平均マージ 1d 20h) (30d で 345 merged PRs)
説明
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.