diff options
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile.dune b/Makefile.dune index 81afa5bb91..cac1bdd6a1 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -7,6 +7,9 @@ # DUNEOPT=--display=short BUILD_CONTEXT=_build/default +COQ_CONFIGURE_PREFIX?=_build/install/default + +export COQ_CONFIGURE_PREFIX help: @echo "Welcome to Coq's Dune-based build system. Targets are:" |