[Pkg-ocaml-maint-commits] [coq-doc] 03/03: new upstream version and minor polishing
Hendrik Tews
hendrik-guest at moszumanska.debian.org
Wed Jul 5 21:02:15 UTC 2017
This is an automated email from the git hooks/post-receive script.
hendrik-guest pushed a commit to branch master
in repository coq-doc.
commit 2dc0095a6bc2cd2b4c4916b19bbe1c55d7a87880
Author: Hendrik Tews <hendrik at askra.de>
Date: Wed Jul 5 22:21:24 2017 +0200
new upstream version and minor polishing
---
debian/.gitignore | 1 +
debian/changelog | 15 +++++++++++++++
debian/control | 16 ++++++++++------
debian/coq-doc-html.doc-base.faq | 4 ++--
debian/coq-doc-html.doc-base.manual | 2 +-
debian/coq-doc-html.install | 1 +
debian/coq-doc-pdf.doc-base.faq | 4 ++--
debian/coq-doc-pdf.doc-base.manual | 2 +-
debian/patches/series | 1 -
debian/patches/unterminated_string_literal | 17 -----------------
10 files changed, 33 insertions(+), 30 deletions(-)
diff --git a/debian/.gitignore b/debian/.gitignore
new file mode 100644
index 0000000..b25c15b
--- /dev/null
+++ b/debian/.gitignore
@@ -0,0 +1 @@
+*~
diff --git a/debian/changelog b/debian/changelog
index 4913d35..c40dacf 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,18 @@
+coq-doc (8.6-1) unstable; urgency=medium
+
+ * Team upload.
+ * New upstream version 8.6 (Closes: #864468)
+ * add myself to uploaders
+ * bump standards version to 4.0.0
+ * fix build dependencies
+ * changed Vcs fields to https
+ * fixed missing axiom picture in FAQ
+ * remove unterminated_string_literal patch (fixed upstream)
+ * updated doc-base entries
+ * added .gitignore in debian dir to ignore editor backups
+
+ -- Hendrik Tews <hendrik at askra.de> Wed, 05 Jul 2017 22:29:28 +0200
+
coq-doc (8.4pl4-2) unstable; urgency=medium
* Team upload
diff --git a/debian/control b/debian/control
index 4c521a6..d2ea2b6 100644
--- a/debian/control
+++ b/debian/control
@@ -4,22 +4,26 @@ Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint at lists.debian.org>
Uploaders:
Samuel Mimram <smimram at debian.org>,
- Stéphane Glondu <glondu at debian.org>
-Standards-Version: 3.9.5
+ Stéphane Glondu <glondu at debian.org>,
+ Hendrik Tews <hendrik at askra.de>
+Standards-Version: 4.0.0
Build-Depends: debhelper (>= 9)
Build-Depends-Indep:
texlive,
texlive-base,
texlive-latex-extra,
- texlive-math-extra,
+ texlive-science,
texlive-lang-french,
texlive-humanities,
hevea (>= 1.05),
+ imagemagick,
+ fig2dev,
camlp5,
- ocaml-nox
+ ocaml-nox,
+ ocaml-findlib
Homepage: http://coq.inria.fr/
-Vcs-Git: git://anonscm.debian.org/pkg-ocaml-maint/packages/coq-doc.git
-Vcs-Browser: http://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/coq-doc.git
+Vcs-Git: https://anonscm.debian.org/cgit/pkg-ocaml-maint/packages/coq-doc.git
+Vcs-Browser: https://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/coq-doc.git
Package: coq-doc
Architecture: all
diff --git a/debian/coq-doc-html.doc-base.faq b/debian/coq-doc-html.doc-base.faq
index 79e34ad..9f4c3ee 100644
--- a/debian/coq-doc-html.doc-base.faq
+++ b/debian/coq-doc-html.doc-base.faq
@@ -1,6 +1,6 @@
Document: coq-faq-html
-Title: Coq Version 8.0 for the Clueless (FAQ)
-Author: Hugo Herbelin, Florent Kirchner, Benjamin Monate, Julien Narboux
+Title: Coq Version 8.4 for the Clueless (FAQ)
+Author: Pierre Castéran, Hugo Herbelin, Florent Kirchner, Benjamin Monate, Julien Narboux
Abstract: This note intends to provide an easy way to get acquainted with the Coq theorem prover. It tries to formulate appropriate answers to some of the questions any newcomers will face, and to give pointers to other references when possible.
Section: Science/Mathematics
diff --git a/debian/coq-doc-html.doc-base.manual b/debian/coq-doc-html.doc-base.manual
index cf7b9a2..f2e242d 100644
--- a/debian/coq-doc-html.doc-base.manual
+++ b/debian/coq-doc-html.doc-base.manual
@@ -1,7 +1,7 @@
Document: coq-manual-html
Title: The Coq Proof Assistant Reference Manual
Author: The Coq Development Team
-Abstract: Reference Manual of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
+Abstract: Reference Manual of version 8.6 of the Coq proof assistant, which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
Section: Science/Mathematics
Format: HTML
diff --git a/debian/coq-doc-html.install b/debian/coq-doc-html.install
index 72c447e..5e680af 100644
--- a/debian/coq-doc-html.install
+++ b/debian/coq-doc-html.install
@@ -1,4 +1,5 @@
doc/refman/html/* usr/share/doc/coq-doc-html/refman
doc/tutorial/Tutorial.v.html usr/share/doc/coq-doc-html
doc/faq/FAQ.v.html usr/share/doc/coq-doc-html
+doc/faq/axioms.png usr/share/doc/coq-doc-html
doc/RecTutorial/RecTutorial.html usr/share/doc/coq-doc-html
diff --git a/debian/coq-doc-pdf.doc-base.faq b/debian/coq-doc-pdf.doc-base.faq
index c09f1dd..8e74790 100644
--- a/debian/coq-doc-pdf.doc-base.faq
+++ b/debian/coq-doc-pdf.doc-base.faq
@@ -1,6 +1,6 @@
Document: coq-faq-pdf
-Title: Coq Version 8.0 for the Clueless (FAQ)
-Author: Hugo Herbelin, Florent Kirchner, Benjamin Monate, Julien Narboux
+Title: Coq Version 8.4 for the Clueless (FAQ)
+Author: Pierre Castéran, Hugo Herbelin, Florent Kirchner, Benjamin Monate, Julien Narboux
Abstract: This note intends to provide an easy way to get acquainted with the Coq theorem prover. It tries to formulate appropriate answers to some of the questions any newcomers will face, and to give pointers to other references when possible.
Section: Science/Mathematics
diff --git a/debian/coq-doc-pdf.doc-base.manual b/debian/coq-doc-pdf.doc-base.manual
index 3b8a8a4..9b2f13a 100644
--- a/debian/coq-doc-pdf.doc-base.manual
+++ b/debian/coq-doc-pdf.doc-base.manual
@@ -1,7 +1,7 @@
Document: coq-manual-pdf
Title: The Coq Proof Assistant Reference Manual
Author: The Coq Development Team
-Abstract: Reference Manual of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
+Abstract: Reference Manual of version 8.6 of the Coq proof assistant, which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
Section: Science/Mathematics
Format: PDF
diff --git a/debian/patches/series b/debian/patches/series
index f0607cd..e69de29 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1 +0,0 @@
-unterminated_string_literal
diff --git a/debian/patches/unterminated_string_literal b/debian/patches/unterminated_string_literal
deleted file mode 100644
index cc1973a..0000000
--- a/debian/patches/unterminated_string_literal
+++ /dev/null
@@ -1,17 +0,0 @@
-Author: Ralf Treinen <treinen at debian.org>
-Description: fix FTBFS "unterminated string literal" with ocaml 4.02.3
-Debian-bug: 813063
-
-Index: coq-doc/kernel/univ.ml
-===================================================================
---- coq-doc.orig/kernel/univ.ml 2016-02-11 08:12:56.448329274 +0100
-+++ coq-doc/kernel/univ.ml 2016-02-11 08:27:43.756005774 +0100
-@@ -226,7 +226,7 @@
-
-
- (* between : UniverseLevel.t -> canonical_arc -> canonical_arc list *)
--(* between u v = {w|u<=w<=v, w canonical} *)
-+(* between u v = { w|u<=w<=v, w canonical } *)
- (* between is the most costly operation *)
-
- let between g arcu arcv =
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq-doc.git
More information about the Pkg-ocaml-maint-commits
mailing list