diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-10-19 12:10:09 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-10-19 15:18:41 +0200 |
| commit | d3bc4be4a7aca149529b8cffae63b3c421bf7118 (patch) | |
| tree | 41af71485ff136b209eb3edb1e66bef678edcfa2 /debian | |
| parent | 6260e57c1e3a6bdbb9fc983ecbd7eecff433dcfa (diff) | |
Add 0002-Fix-mixed-implicit-and-normal-rules.patch
Diffstat (limited to 'debian')
| -rw-r--r-- | debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch | 85 | ||||
| -rw-r--r-- | debian/patches/series | 1 |
2 files changed, 86 insertions, 0 deletions
diff --git a/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch b/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch new file mode 100644 index 00000000..79c1a22b --- /dev/null +++ b/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch @@ -0,0 +1,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 + + +-- diff --git a/debian/patches/series b/debian/patches/series index c65680e0..d2880009 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1 +1,2 @@ 0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch +0002-Fix-mixed-implicit-and-normal-rules.patch |