aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/Makefile.coq-makefile
diff options
context:
space:
mode:
authorCyril Cohen2018-07-31 10:37:25 +0200
committerCyril Cohen2018-07-31 11:38:53 +0200
commit4199c23da311e612cb1ae45cf5519b5f3947c3b3 (patch)
tree4e887d501dd9d1f5d983ca236cbadcd803c8a091 /mathcomp/ssreflect/Makefile.coq-makefile
parent6c6c907438f4179ac335e7daa9f1ed030c0c8259 (diff)
Rework the whole Makefile architecture
- Cleanup, refactoring and generalize the makefile architecture - Reuses @strub math-comp/analysis Makefile / Makefile.common organization - As #174, this fixes #88, but looks more stable than trying to fix the use of the MAKEFLAGS internal variable
Diffstat (limited to 'mathcomp/ssreflect/Makefile.coq-makefile')
-rw-r--r--mathcomp/ssreflect/Makefile.coq-makefile5
1 files changed, 2 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile
index ba0e5d7..e904236 100644
--- a/mathcomp/ssreflect/Makefile.coq-makefile
+++ b/mathcomp/ssreflect/Makefile.coq-makefile
@@ -1,4 +1,4 @@
-define coqmakefile
+define prepare_coqmakefile
(echo "Generating Makefile.coq for Coq $(V) with COQBIN=$(COQBIN)";\
if [ "$$OS" = "Windows_NT" ]; then LN=cp; else LN="ln -sfr"; fi;\
MLLIB=;\
@@ -26,7 +26,6 @@ define coqmakefile
MLLIB=ssreflect_plugin.mlpack;\
EXTRA="ssreflect.ml4";\
;;\
- esac;\
- $(COQBIN)coq_makefile -f Make $$MLLIB $$EXTRA -o Makefile.coq)
+ esac
endef