1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
From: Stephane Glondu <steph@glondu.net>
Date: Tue, 19 Oct 2010 12:00:55 +0200
Subject: [PATCH] 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
Signed-off-by: Stephane Glondu <steph@glondu.net>
---
Makefile | 10 ++++++++++
Makefile.common | 15 +++++++++------
2 files changed, 19 insertions(+), 6 deletions(-)
diff --git a/Makefile b/Makefile
index 975ece0..908dbd6 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
--
|
