aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/ssreflect')
-rw-r--r--mathcomp/ssreflect/Makefile2
-rw-r--r--mathcomp/ssreflect/Makefile.coq-makefile8
2 files changed, 5 insertions, 5 deletions
diff --git a/mathcomp/ssreflect/Makefile b/mathcomp/ssreflect/Makefile
index af5a204..c588920 100644
--- a/mathcomp/ssreflect/Makefile
+++ b/mathcomp/ssreflect/Makefile
@@ -21,7 +21,7 @@ MAKEFLAGS+=-B
.DEFAULT_GOAL := all
%:
- $(H)[ -e Makefile.coq ] || $(call coqmakefile)
+ $(H)[ -e Makefile.coq ] || $(call coqmakefile,.)
# Override COQDEP to find only the "right" copy .ml files
$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-f Makefile.coq $* \
diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile
index 99f3d6b..9cce300 100644
--- a/mathcomp/ssreflect/Makefile.coq-makefile
+++ b/mathcomp/ssreflect/Makefile.coq-makefile
@@ -1,9 +1,9 @@
define coqmakefile
(echo "Generating Makefile.coq for Coq $(V) with COQBIN=$(COQBIN)";\
- ln -sf plugin/$(V)/ssreflect.mllib .;\
- ln -sf plugin/$(V)/ssrmatching.mli .;\
- ln -sf plugin/$(V)/ssrmatching.ml4 .;\
- ln -sf plugin/$(V)/ssreflect.ml4 .;\
+ ln -sf $(1)/plugin/$(V)/ssreflect.mllib .;\
+ ln -sf $(1)/plugin/$(V)/ssrmatching.mli .;\
+ ln -sf $(1)/plugin/$(V)/ssrmatching.ml4 .;\
+ ln -sf $(1)/plugin/$(V)/ssreflect.ml4 .;\
$(COQBIN)coq_makefile -f Make -o Makefile.coq)
endef