85 lines
2.7 KiB
Diff
85 lines
2.7 KiB
Diff
|
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
|
||
|
|
Date: Tue, 19 Oct 2010 13:22:08 +0000 (+0000)
|
||
|
|
Subject: Fix mixed implicit and normal rules
|
||
|
|
X-Git-Url: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq%2Fcoq-svn.git;a=commitdiff_plain;h=86eb08bad450dd3fa77b11e4a34d2f493ab80d85
|
||
|
|
|
||
|
|
Fix mixed implicit and normal rules
|
||
|
|
|
||
|
|
This fixes build with GNU Make 3.82. See threads:
|
||
|
|
|
||
|
|
https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html
|
||
|
|
http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912
|
||
|
|
|
||
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.3@13566 85f007b7-540e-0410-9357-904b9bb8a0f7
|
||
|
|
---
|
||
|
|
|
||
|
|
diff --git a/Makefile b/Makefile
|
||
|
|
index b1edc01..ea73c51 100644
|
||
|
|
--- a/Makefile
|
||
|
|
+++ b/Makefile
|
||
|
|
@@ -160,9 +160,19 @@ else
|
||
|
|
stage1 $(STAGE1_TARGETS) : always
|
||
|
|
$(call stage-template,1)
|
||
|
|
|
||
|
|
+ifneq (,$(STAGE1_IMPLICITS))
|
||
|
|
+$(STAGE1_IMPLICITS) : always
|
||
|
|
+ $(call stage-template,1)
|
||
|
|
+endif
|
||
|
|
+
|
||
|
|
stage2 $(STAGE2_TARGETS) : stage1
|
||
|
|
$(call stage-template,2)
|
||
|
|
|
||
|
|
+ifneq (,$(STAGE2_IMPLICITS))
|
||
|
|
+$(STAGE2_IMPLICITS) : stage1
|
||
|
|
+ $(call stage-template,2)
|
||
|
|
+endif
|
||
|
|
+
|
||
|
|
# Nota:
|
||
|
|
# - world is one of the targets in $(STAGE2_TARGETS), hence launching
|
||
|
|
# "make" or "make world" leads to recursion into stage1 then stage2
|
||
|
|
diff --git a/Makefile.common b/Makefile.common
|
||
|
|
index cc38980..46bf217 100644
|
||
|
|
--- a/Makefile.common
|
||
|
|
+++ b/Makefile.common
|
||
|
|
@@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y")
|
||
|
|
|
||
|
|
SOURCEDOCDIR=dev/source-doc
|
||
|
|
|
||
|
|
-CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
|
||
|
|
+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot
|
||
|
|
|
||
|
|
### Targets forwarded by Makefile to a specific stage:
|
||
|
|
|
||
|
|
@@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
|
||
|
|
STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
|
||
|
|
$(GENFILES) \
|
||
|
|
source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
|
||
|
|
- $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
|
||
|
|
+ $(STAGE1_ML4:.ml4=.ml4-preprocessed)
|
||
|
|
+
|
||
|
|
+STAGE1_IMPLICITS:=
|
||
|
|
|
||
|
|
ifdef CM_STAGE1
|
||
|
|
- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
|
||
|
|
+ STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
|
||
|
|
endif
|
||
|
|
|
||
|
|
## Enumeration of targets that require being done at stage2
|
||
|
|
@@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
|
||
|
|
printers debug initplugins plugins \
|
||
|
|
world install coqide coqide-files coq coqlib \
|
||
|
|
coqlight states check init theories theories-light \
|
||
|
|
- $(DOC_TARGETS) $(VO_TARGETS) validate \
|
||
|
|
- %.vo %.glob states/% install-% %.ml4-preprocessed \
|
||
|
|
+ $(DOC_TARGETS) $(VO_TARGETS) validate
|
||
|
|
+
|
||
|
|
+STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \
|
||
|
|
$(DOC_TARGET_PATTERNS)
|
||
|
|
|
||
|
|
ifndef CM_STAGE1
|
||
|
|
- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS)
|
||
|
|
+ STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
|
||
|
|
endif
|
||
|
|
|
||
|
|
|