[Pkg-ocaml-maint-commits] r952 - packages/coq/trunk/debian

[Samuel Mimram]

Author: smimram-guest
Date: 2005-02-01 22:58:59 +0100 (Tue, 01 Feb 2005)
New Revision: 952

Modified:
   packages/coq/trunk/debian/TODO.Debian
   packages/coq/trunk/debian/copyright
   packages/coq/trunk/debian/rules
Log:
Better handling of arch-indep packages.

Modified: packages/coq/trunk/debian/TODO.Debian
===================================================================
--- packages/coq/trunk/debian/TODO.Debian	2005-02-01 08:04:02 UTC (rev 951)
+++ packages/coq/trunk/debian/TODO.Debian	2005-02-01 21:58:59 UTC (rev 952)
@@ -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.

Modified: packages/coq/trunk/debian/copyright
===================================================================
--- packages/coq/trunk/debian/copyright	2005-02-01 08:04:02 UTC (rev 951)
+++ packages/coq/trunk/debian/copyright	2005-02-01 21:58:59 UTC (rev 952)
@@ -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 @@
         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

Modified: packages/coq/trunk/debian/rules
===================================================================
--- packages/coq/trunk/debian/rules	2005-02-01 08:04:02 UTC (rev 951)
+++ packages/coq/trunk/debian/rules	2005-02-01 21:58:59 UTC (rev 952)
@@ -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 @@
 	# 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 @@
 		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