Reintroduce compatibility with old versions of GNU make

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9497 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 21 insertions, 12 deletions

diff --git a/INSTALL b/INSTALL
index fc900e05f..fbfee163e 100644
--- a/INSTALL
+++ b/INSTALL
@@ -11,13 +11,6 @@ WHAT DO YOU NEED ?
      - Objective Caml version 3.07 or later
        (available at http://caml.inria.fr/)
 
-     - GNU Make version 3.80 or later
-       (available at http://www.gnu.org/software/make/, but also a
-        standard or optional add-on part to most Unices and Unix
-        clones, sometimes under the name "gmake".)
-
-     - A C compiler
-
    Until now, it has mainly been tested on Sun workstations running Solaris,
    DEC alpha and Pentium workstations running Linux. By FTP, Coq comes
    as a single compressed tar-file. You have probably already
diff --git a/Makefile b/Makefile
index 776fff914..62f620262 100644
--- a/Makefile
+++ b/Makefile
@@ -347,6 +347,18 @@ OBJSCMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \
         $(HIGHTACTICS) $(USERTACMO) $(CONTRIB)
 
 ###########################################################################
+# Infrastructure for the rest of the Makefile
+###########################################################################
+
+define order-only-template
+ ifeq "order-only" "$(1)"
+   ORDER_ONLY_SEP:=|
+ endif
+endef
+
+$(foreach f,$(.FEATURES),$(eval $(call order-only-template,$(f))))
+
+###########################################################################
 # Compilation option for .c files 
 ###########################################################################
 
@@ -421,7 +433,7 @@ $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(USERTACCMO)
 	$(SHOW)'COQMKTOP -o $@'	
 	$(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@
 
-$(COQTOP): | $(BESTCOQTOP)
+$(COQTOP): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
 	cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
 
 # coqmktop 
@@ -439,7 +451,7 @@ $(COQMKTOPOPT): $(COQMKTOPCMX)
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa \
           $(COQMKTOPCMX) $(OSDEPLIBS)
 
-$(COQMKTOP): | $(BESTCOQMKTOP)
+$(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP)
 	cd bin; ln -sf coqmktop.$(BEST)$(EXE) coqmktop$(EXE)
 
 
@@ -465,7 +477,7 @@ $(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ unix.cmxa $(COQCCMX) $(OSDEPLIBS)
 
-$(COQC): | $(BESTCOQC)
+$(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC)
 	cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE)
 
 
@@ -1110,9 +1122,13 @@ ALLVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO)
 SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v
 
 ifdef NO_RECOMPILE_LIB
- VO_TOOLS_DEP += |
+ ifdef ORDER_ONLY_SEP
+  VO_TOOLS_DEP += $(ORDER_ONLY_SEP)
+ else
+  $(error NO_RECOMPILE_LIB needs GNU make version 3.80 or later; that is a version that supports order-only dependencies)
+ endif
 endif
- VO_TOOLS_DEP += $(BESTCOQTOP)
+VO_TOOLS_DEP += $(BESTCOQTOP)
 ifdef COQ_XML
  VO_TOOLS_DEP += $(COQDOC)
 endif