Fix build from source when a dune-project file is presented in the parent directory

[kit-ty-kate]

Fixes #4537

[rjbou]

Thanks!

[rjbou]

Just a question, is there a reason to not use DUNE_ARGS to add it one place instead on each dune call ?

[dra27]

Just a question, is there a reason to not use DUNE_ARGS to add it one place instead on each dune call ?

🌴 You don't want the user to be able to change it - DUNE_ARGS is for extra arguments, not mandatory ones. It could go in another variable like DUNE_CMD = $(DUNE) --profile=$(...) --root=. but we already didn't do that for --profile

[dra27]

This would need to be slightly more complicated - the idea was that you can say make DUNE_PROFILE=dev

[kit-ty-kate]

we could still have something like that:

ifeq ($(DUNE_PROFILE),release)
DUNE_PROFILE_ARG=--release
else
DUNE_PROFILE_ARG=--profile=$(DUNE_PROFILE)
endif

[dra27]

Indeed, that was my slightly more complicated 🙂

[dra27]

Good to go when CI’s ready

[rjbou]

@AltGr can you take a look (and update PR) to be sure to not broke the new dune tests makefiles 😇

[dra27]

Rebased and I (throughly) checked all the dune calls - good to go, as long as CI agrees.