summaryrefslogtreecommitdiff
path: root/debian
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-19 12:10:09 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-19 15:18:41 +0200
commitd3bc4be4a7aca149529b8cffae63b3c421bf7118 (patch)
tree41af71485ff136b209eb3edb1e66bef678edcfa2 /debian
parent6260e57c1e3a6bdbb9fc983ecbd7eecff433dcfa (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.patch85
-rw-r--r--debian/patches/series1
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