diff options
Diffstat (limited to 'pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch')
-rw-r--r-- | pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch | 84 |
1 files changed, 0 insertions, 84 deletions
diff --git a/pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch b/pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch deleted file mode 100644 index 5176aa33ec8a..000000000000 --- a/pkgs/applications/science/logic/coq/coq-8.3-make-3.82-compat.patch +++ /dev/null @@ -1,84 +0,0 @@ -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 - - |