summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--debian/changelog6
-rw-r--r--debian/coq-libs.dirs2
-rw-r--r--debian/coq-libs.doc-base9
-rwxr-xr-xdebian/patches/browser.dpatch19
-rwxr-xr-xdebian/patches/coqdoc_stdlib.dpatch19
-rwxr-xr-xdebian/patches/makefile.dpatch20
6 files changed, 75 insertions, 0 deletions
diff --git a/debian/changelog b/debian/changelog
index a161de61..9ced581a 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,9 @@
+coq (8.1+dfsg-3) unstable; urgency=low
+
+ * Uploading to unstable.
+
+ -- Samuel Mimram <smimram@debian.org> Mon, 09 Apr 2007 16:48:46 +0200
+
coq (8.1+dfsg-2) experimental; urgency=low
* Added cmxa-install.dpatch to install cmxa only on native archs,
diff --git a/debian/coq-libs.dirs b/debian/coq-libs.dirs
new file mode 100644
index 00000000..aadcf27a
--- /dev/null
+++ b/debian/coq-libs.dirs
@@ -0,0 +1,2 @@
+usr/share/doc/coq-libs
+usr/share/doc/coq
diff --git a/debian/coq-libs.doc-base b/debian/coq-libs.doc-base
new file mode 100644
index 00000000..1a62a262
--- /dev/null
+++ b/debian/coq-libs.doc-base
@@ -0,0 +1,9 @@
+Document: coq-library
+Title: The Coq Standard Library
+Author: The Coq Development Team
+Abstract: Standard Library documentation 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.
+Section: Apps/Math
+
+Format: HTML
+Index: /usr/share/doc/coq-libs/html/index.html
+Files: /usr/share/doc/coq-libs/html/*.html
diff --git a/debian/patches/browser.dpatch b/debian/patches/browser.dpatch
new file mode 100755
index 00000000..ba55f3de
--- /dev/null
+++ b/debian/patches/browser.dpatch
@@ -0,0 +1,19 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## browser.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Use the default Debian browser for help.
+
+@DPATCH@
+diff -urNad coq-8.0pl3+8.1alpha~/lib/options.ml coq-8.0pl3+8.1alpha/lib/options.ml
+--- coq-8.0pl3+8.1alpha~/lib/options.ml 2005-12-26 20:07:21.000000000 +0000
++++ coq-8.0pl3+8.1alpha/lib/options.ml 2006-04-29 16:06:20.000000000 +0000
+@@ -117,7 +117,4 @@
+ "\" must contain exactly one placeholder \"%s\".")
+ else pre,post
+ with
+- Not_found ->
+- if Sys.os_type = "Win32"
+- then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
+- else "netscape -remote \"OpenURL(", ")\""
++ Not_found -> "/usr/bin/x-www-browser ", ""
diff --git a/debian/patches/coqdoc_stdlib.dpatch b/debian/patches/coqdoc_stdlib.dpatch
new file mode 100755
index 00000000..fb618f56
--- /dev/null
+++ b/debian/patches/coqdoc_stdlib.dpatch
@@ -0,0 +1,19 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## coqdoc_stdlib.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Add an option to coqdoc to be able to use a custom stdlib path in order
+## DP: to be able to build the documentation before coqdoc is installed.
+
+@DPATCH@
+diff -urNad coq-8.0pl3+8.1beta~/doc/Makefile coq-8.0pl3+8.1beta/doc/Makefile
+--- coq-8.0pl3+8.1beta~/doc/Makefile 2006-06-16 13:02:33.000000000 +0000
++++ coq-8.0pl3+8.1beta/doc/Makefile 2006-06-16 13:19:11.000000000 +0000
+@@ -216,6 +216,7 @@
+ mkdir stdlib/html
+ (cd stdlib/html;\
+ $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\
++ --coqlib_path $(COQTOP) \
+ -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v)
+ mv stdlib/html/index.html stdlib/index-body.html
+
diff --git a/debian/patches/makefile.dpatch b/debian/patches/makefile.dpatch
new file mode 100755
index 00000000..b656a9bb
--- /dev/null
+++ b/debian/patches/makefile.dpatch
@@ -0,0 +1,20 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## makefile.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Do not use ocamlopt to test grammar.cma, we don't want to use ocamlopt
+## DP: when compiling on non-native archs.
+
+@DPATCH@
+diff -urNad coq-8.0pl3+8.1alpha~/Makefile coq-8.0pl3+8.1alpha/Makefile
+--- coq-8.0pl3+8.1alpha~/Makefile 2006-04-07 15:08:12.000000000 +0000
++++ coq-8.0pl3+8.1alpha/Makefile 2006-04-30 11:41:09.000000000 +0000
+@@ -1401,7 +1401,7 @@
+ parsing/grammar.cma: $(GRAMMARCMO)
+ $(SHOW)'Testing $@'
+ @touch test.ml4
+- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
++ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
+ @rm -f test-grammar test.*
+ $(SHOW)'OCAMLC -a $@'
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@