Metriche repository
- Star
- (1882 stelle)
- Metriche merge PR
- (Merge medio 1g 20h) (345 PR mergiate in 30 g)
Descrizione
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.