aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
authorCyril Cohen2018-07-31 15:58:21 +0200
committerCyril Cohen2018-07-31 15:58:21 +0200
commit1a4a4b1cd2407ffd8b76fb544596d1c91ea63a4b (patch)
tree93da9bb6016bdc5fe5b82b9ebc17e53b98a4d085 /mathcomp
parent7d7b0688c818c5dde68d2b2bfc8ba3aecfe017d6 (diff)
some things should always be done
Diffstat (limited to 'mathcomp')
-rw-r--r--mathcomp/Makefile.common6
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