diff options
| author | Cyril Cohen | 2018-07-31 15:58:21 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2018-07-31 15:58:21 +0200 |
| commit | 1a4a4b1cd2407ffd8b76fb544596d1c91ea63a4b (patch) | |
| tree | 93da9bb6016bdc5fe5b82b9ebc17e53b98a4d085 /mathcomp/Makefile.common | |
| parent | 7d7b0688c818c5dde68d2b2bfc8ba3aecfe017d6 (diff) | |
some things should always be done
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 |