summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-11-21 19:43:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-11-21 19:43:47 +0000
commit06e68c3dcfcda1479176630061da728fb754f8d3 (patch)
tree0d56d47be731f33b53be7427d53355f07a099a85
parent44032630776b3315fc377d287e76580de759fd47 (diff)
Updated to OCaml 3.09.0.debian/8.0pl2-4
-rw-r--r--debian/changelog9
-rw-r--r--debian/control6
-rw-r--r--debian/patches/00list1
-rwxr-xr-xdebian/patches/ocaml309.dpatch24
4 files changed, 37 insertions, 3 deletions
diff --git a/debian/changelog b/debian/changelog
index bb23aae2..61876571 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,12 @@
+coq (8.0pl2-4) unstable; urgency=low
+
+ * Added ocaml309.dpatch patch to compile cleanly with OCaml 3.09,
+ closes: #340185.
+ * Removed recommends on coq-doc which is not in main anymore.
+ * Updated standards version to 3.6.2, no changes needed.
+
+ -- Samuel Mimram <smimram@debian.org> Mon, 21 Nov 2005 19:52:53 +0100
+
coq (8.0pl2-3) unstable; urgency=low
* Added text_view_typing_error patch to avoid a typing error and solve the
diff --git a/debian/control b/debian/control
index 00918f5c..e6e71135 100644
--- a/debian/control
+++ b/debian/control
@@ -3,13 +3,13 @@ Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders: Ralf Treinen <treinen@debian.org>, Sven Luther <luther@debian.org>, Remi Vanicat <vanicat@debian.org>, Stefano Zacchiroli <zack@debian.org>, Samuel Mimram <smimram@debian.org>
-Standards-Version: 3.6.1.1
-Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.08.2), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0)
+Standards-Version: 3.6.2
+Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0)
Package: coq
Architecture: any
Depends: ${shlibs:Depends}, coq-libs (= ${Source-Version})
-Recommends: coq-doc, coqide | proofgeneral-coq
+Recommends: coqide | proofgeneral-coq
Suggests: ocaml-nox (>= 3.08), proofgeneral-coq, ledit, cle
Description: proof assistant for higher-order logic (toplevel and compiler)
Coq is a proof assistant for higher-order logic, which allows the
diff --git a/debian/patches/00list b/debian/patches/00list
index ea23d9d7..ff826cb0 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1 +1,2 @@
+ocaml309
text_view_typing_error
diff --git a/debian/patches/ocaml309.dpatch b/debian/patches/ocaml309.dpatch
new file mode 100755
index 00000000..e116bf0e
--- /dev/null
+++ b/debian/patches/ocaml309.dpatch
@@ -0,0 +1,24 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## ocaml309.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Correct a compilation issue with OCaml 3.09.
+
+@DPATCH@
+diff -urNad coq-8.0pl2~/Makefile coq-8.0pl2/Makefile
+--- coq-8.0pl2~/Makefile 2005-01-21 18:15:12.000000000 +0100
++++ coq-8.0pl2/Makefile 2005-11-21 19:51:38.000000000 +0100
+@@ -1453,11 +1453,11 @@
+
+ .ml4.cmx:
+ $(SHOW)'OCAMLOPT4 $<'
+- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
++ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -loc loc -impl" -c -impl $<
+
+ .ml4.cmo:
+ $(SHOW)'OCAMLC4 $<'
+- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
++ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -loc loc -impl" -c -impl $<
+
+ #.v.vo:
+ # $(BOOTCOQTOP) -compile $*