summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-02-01 21:58:59 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-02-01 21:58:59 +0000
commit3b182903454caa27cd34fc38c594970a800dc9a1 (patch)
tree0cb1e18612d495de06199f9d29ef4dd8764bc68e
parent6b61b68d5822575015583047e1d266b8257e35d5 (diff)
Better handling of arch-indep packages.
-rw-r--r--debian/TODO.Debian1
-rw-r--r--debian/copyright8
-rwxr-xr-xdebian/rules31
3 files changed, 28 insertions, 12 deletions
diff --git a/debian/TODO.Debian b/debian/TODO.Debian
index 61d5189d..5cba552e 100644
--- a/debian/TODO.Debian
+++ b/debian/TODO.Debian
@@ -1,3 +1,4 @@
* Move the coqide stuff from /usr/lib/coq/ide to /usr/share/coqide. The variable
lib_ide should be changed to do that.
+* Remove the .byte files on native archs.
diff --git a/debian/copyright b/debian/copyright
index f4d56d47..c53b8733 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -1,14 +1,14 @@
This package was debianized by Fernando Sanchez <fer@debian.org>
-I was downloaded from
+It was downloaded from
-ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0pl1
+ftp://ftp.inria.fr/INRIA/LogiCal/coq/current
The Coq proof assistant V7 and V8 includes software developed by the
Coq development team inside the LogiCal project, at INRIA, CNRS and
University Paris Sud.
-Copyright 1999-2004 The Coq development team,
+Copyright 1999-2005 The Coq development team,
INRIA-CNRS, University Paris Sud, All rights reserved.
This product includes also software developed by
@@ -17,7 +17,7 @@ This product includes also software developed by
Pierre Crégut, France Telecom R & D (contrib/omega and contrib/romega)
Pierre Courtieu, Lemme (contrib/funind)
Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier)
- Claudio Sacerdoti Coen, HELM, University of Bologna, (contrib/xml)
+ Claudio Sacerdoti Coen, HELM, University of Bologna (contrib/xml)
Coq includes a tactic Jp based on JProver, a theorem prover for
first-order intuitionistic logic. Jprover was originally implemented
diff --git a/debian/rules b/debian/rules
index dbc78be0..9c65c9b3 100755
--- a/debian/rules
+++ b/debian/rules
@@ -1,6 +1,13 @@
#!/usr/bin/make -f
# debian/rules for coq
+# Uncomment this to turn on verbose mode.
+#export DH_VERBOSE=1
+
+# This has to be exported to make some magic below work.
+export DH_OPTIONS
+
+# We want to use dpatch
include /usr/share/dpatch/dpatch.make
COQPREF=$(CURDIR)/debian/tmp
@@ -86,20 +93,30 @@ install: build
# These are installed as docs
rm -f $(COQPREF)/usr/lib/coq/ide/utf8.v $(COQPREF)/usr/lib/coq/ide/FAQ
-binary-indep: build install
+ dh_install --sourcedir=$(COQPREF) --list-missing
-binary-arch: build install
+binary-common:
dh_testdir
dh_testroot
dh_installdocs
dh_installemacsen
+ dh_installman
dh_installchangelogs CHANGES
- dh_install --sourcedir=$(COQPREF) --list-missing
dh_link
dh_compress
dh_fixperms
dh_installdeb
dh_shlibdeps
+
+binary-indep: build install
+ $(MAKE) -f debian/rules DH_OPTIONS=-i binary-common
+ dh_gencontrol -pcoq-libs
+ dh_gencontrol -pcoq7-libs
+ dh_md5sums -i
+ dh_builddeb -i
+
+binary-arch: build install
+ $(MAKE) -f debian/rules DH_OPTIONS=-a binary-common
if [ -e opt-stamp ]; then \
dh_gencontrol -pcoq -u-Vocaml:Runtime=""; \
dh_gencontrol -pcoqide -u-Vocaml:Runtime=""; \
@@ -107,10 +124,8 @@ binary-arch: build install
dh_gencontrol -pcoq -u-Vocaml:Runtime="ocaml-base-nox-3.08"; \
dh_gencontrol -pcoqide -u-Vocaml:Runtime="ocaml-base-nox-3.08"; \
fi
- dh_gencontrol -pcoq-libs
- dh_gencontrol -pcoq7-libs
- dh_md5sums
- dh_builddeb
+ dh_md5sums -s
+ dh_builddeb -s
binary: binary-indep binary-arch
-.PHONY: build clean binary-indep binary-arch binary install configure
+.PHONY: build clean binary-indep binary-arch binary-common binary install configure