acceptedgood first issue
Métriques du dépôt
- Stars
- (1 882 étoiles)
- Métriques de merge PR
- (Merge moyen 1j 20h) (345 PRs mergées en 30 j)
Description
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.