Uploading to unstable.debian/8.1+dfsg-3

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 $@