diff options
| author | Théo Zimmermann | 2018-09-21 16:22:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-21 16:22:32 +0200 |
| commit | 508265318ad39d2962587af4e10f79f4cf4cf4c6 (patch) | |
| tree | d4a32174d207668881e3de350863764760541f5f /Makefile.dune | |
| parent | 80b0619e81bec85e8f37b4ee9f8e4d5faa3eae13 (diff) | |
| parent | 81e4c7152da598c1750e7881b197a6fcf54e818d (diff) | |
Merge PR #8443: [opam] [dune] Fix typo + set prefix for configure.
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:" |