diff options
| -rw-r--r-- | debian/TODO.Debian | 1 | ||||
| -rw-r--r-- | debian/copyright | 8 | ||||
| -rwxr-xr-x | debian/rules | 31 |
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 |