acceptedgood first issue
Repository-Metriken
- Stars
- (1.882 Sterne)
- PR-Merge-Metriken
- (Durchschn. Merge 1T 20h) (345 gemergte PRs in 30 T)
Beschreibung
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.