From 1a4a4b1cd2407ffd8b76fb544596d1c91ea63a4b Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 31 Jul 2018 15:58:21 +0200
Subject: some things should always be done

---
 mathcomp/Makefile.common | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'mathcomp/Makefile.common')

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
-- 
cgit v1.2.3