diff options
Diffstat (limited to 'mathcomp/Makefile.common')
| -rw-r--r-- | mathcomp/Makefile.common | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index ea3d85c..557a05b 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -27,6 +27,8 @@ Makefile.coq: $(BEFOREMAKEFILE) Makefile Makefile.this: $(BEFOREMAKEFILES) Makefile.coq $(AFTERMAKEFILES) cat $(BEFOREMAKEFILES) Makefile.coq $(AFTERMAKEFILES) > Makefile.this + +__always__: Makefile.this # -------------------------------------------------------------------- config: sub-config this-config Makefile.this @@ -39,7 +41,7 @@ distclean: sub-distclean this-distclean # -------------------------------------------------------------------- .PHONY: this-config this-build this-distclean this-clean -this-build:: config +this-build:: __always__ +$(COQMAKE) this-distclean:: this-clean $(OTHERCLEAN) @@ -51,7 +53,7 @@ this-clean:: # -------------------------------------------------------------------- .PHONY: install -install: +install: __always__ $(COQMAKE) install # -------------------------------------------------------------------- .PHONY: count |