You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In input.ml we use _build as a hardcoded value for search. However, some users may override DUNE_BUILD_DIR or pass it as a flag to dune as per dune docs.
This issue is a request to use DUNE_BUILD_DIR instead of _build. Note, that DUNE_BUILD_DIR=_build by default.
Let me know if this change would make sense and you'd be happy for us to contribute it!
Best,
Max.
The text was updated successfully, but these errors were encountered:
Hi! I think that makes sense. I would merge such a change. It looks like DUNE_BUILD_DIR has been around since Dune 1.0.0. However, we should probably fall back to searching in a potential _build directory, as now, if the environment variable is undefined for some reason.
If a user passes in --build-dir foo, is DUNE_BUILD_DIR set to foo?
Hi.
In input.ml we use
_build
as a hardcoded value for search. However, some users may overrideDUNE_BUILD_DIR
or pass it as a flag to dune as per dune docs.This issue is a request to use
DUNE_BUILD_DIR
instead of_build
. Note, thatDUNE_BUILD_DIR=_build
by default.Let me know if this change would make sense and you'd be happy for us to contribute it!
Best,
Max.
The text was updated successfully, but these errors were encountered: