diff options
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Makefile.dune b/Makefile.dune index cac1bdd6a1..81afa5bb91 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -7,9 +7,6 @@ # 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:" |