summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-12-03 11:21:58 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-12-03 11:40:45 +0100
commit668a6055913e047843f505f09c89a8a7badd4dff (patch)
treee77b8f494a0dd3b1ae1240d3710ed60fa4689199
parentf8fd65f3e3e349d00c4d2b38f625564af7a093c6 (diff)
Switch to dh-ocaml 0.9
-rw-r--r--debian/changelog6
-rw-r--r--debian/control27
-rwxr-xr-xdebian/rules12
3 files changed, 24 insertions, 21 deletions
diff --git a/debian/changelog b/debian/changelog
index 8da624c6..11765483 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,8 +1,12 @@
coq (8.2.pl1+dfsg-4) UNRELEASED; urgency=low
+ [ Stefano Zacchiroli ]
* debian/control: fix typo in long description (Closes: #557458)
- -- Stefano Zacchiroli <zack@debian.org> Sun, 22 Nov 2009 16:26:20 +0100
+ [ Stéphane Glondu ]
+ * Switch to dh-ocaml 0.9
+
+ -- Stéphane Glondu <glondu@debian.org> Thu, 03 Dec 2009 11:21:27 +0100
coq (8.2.pl1+dfsg-3) unstable; urgency=low
diff --git a/debian/control b/debian/control
index ee9cded4..0e35df81 100644
--- a/debian/control
+++ b/debian/control
@@ -12,12 +12,11 @@ Standards-Version: 3.8.3
Build-Depends:
debhelper (>= 7),
quilt (>= 0.46-7~),
- dpkg-dev (>= 1.13.19),
- dh-ocaml (>= 0.4.1),
- ocaml-nox (>= 3.11.0-5),
+ dh-ocaml (>= 0.9~),
+ ocaml-nox (>= 3.11.1-3~),
ocaml-best-compilers,
- camlp5 (>= 5.12),
- liblablgtk2-ocaml-dev (>= 2.12.0-3),
+ camlp5 (>= 5.12-2~),
+ liblablgtk2-ocaml-dev (>= 2.14),
texlive-latex-extra,
hevea (>= 1.10-7)
Homepage: http://coq.inria.fr/
@@ -27,11 +26,11 @@ Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/coq.git
Package: coq
Architecture: any
Depends:
- ${shlibs:Depends},
- ${misc:Depends},
- ocaml-base-nox-${F:OCamlABI},
coq-theories (= ${source:Version}),
- emacsen-common
+ emacsen-common,
+ ${ocaml:Depends},
+ ${shlibs:Depends},
+ ${misc:Depends}
Provides: coq-${F:CoqABI}
Recommends: coqide | proofgeneral-coq
Suggests:
@@ -58,10 +57,9 @@ Description: proof assistant for higher-order logic (toplevel and compiler)
Package: coqide
Architecture: any
Depends:
- ${shlibs:Depends},
coq (= ${binary:Version}),
- ocaml-base-nox-${F:OCamlABI},
- liblablgtk2-ocaml,
+ ${ocaml:Depends},
+ ${shlibs:Depends},
${misc:Depends}
Description: proof assistant for higher-order logic (gtk interface)
Coq is a proof assistant for higher-order logic, which allows the
@@ -89,10 +87,11 @@ Package: libcoq-ocaml-dev
Section: ocaml
Architecture: any
Depends:
- ${shlibs:Depends},
coq (= ${binary:Version}),
- ocaml-nox-${F:OCamlABI},
+ ${ocaml:Depends},
+ ${shlibs:Depends},
${misc:Depends}
+Provides: ${ocaml:Provides}
Conflicts: coq (<< 8.2-1+dfsg-1), coq-libs
Replaces: coq (<< 8.2-1+dfsg-1), coq-libs
Description: development libraries and tools for Coq
diff --git a/debian/rules b/debian/rules
index 71b8d68c..4f907015 100755
--- a/debian/rules
+++ b/debian/rules
@@ -14,7 +14,7 @@ export CAML_LD_LIBRARY_PATH = $(shell pwd)/kernel/byterun
# Show full commands when building Coq
export VERBOSE=1
-include /usr/share/ocaml/ocamlinit.mk
+include /usr/share/ocaml/ocamlvars.mk
HTMLDOC := doc/stdlib/html/index.html
@@ -31,14 +31,14 @@ CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \
--browser "/usr/bin/x-www-browser %s &" \
--with-doc no --coqrunbyteflags "-dllib -lcoqrun"
-OCAMLINIT_SED += \
+export OCAMLINIT_SED += \
-e 's%@CoqVersion@%$(COQ_VERSION)%' \
-e 's%@CoqABI@%$(COQ_ABI)%'
-DH := dh --with quilt
+DH := dh --with quilt,ocaml
configure: configure-stamp
-configure-stamp: ocamlinit-stamp
+configure-stamp:
$(DH) build --before dh_auto_configure
./configure $(CONFIGUREOPTS)
touch $@
@@ -83,7 +83,7 @@ install-stamp: build-stamp
done
touch $@
-clean: ocamlinit-clean
+clean:
$(DH) $@
binary-indep: install-stamp
@@ -93,4 +93,4 @@ binary-arch: install-stamp
$(DH) $@
binary: binary-indep binary-arch
-.PHONY: build clean binary-indep binary-arch binary install configure ocamlinit
+.PHONY: build clean binary-indep binary-arch binary install configure