The following commit has been merged in the master branch:
commit 280b58b25462cd9f8e33f96ff76e84cf22eb465c
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 15:29:35 2008 +0200
Move patch-stamp as a prerequisite of configure-stamp
diff --git a/debian/rules b/debian/rules
index 8075e71..e50ad14 100755
--- a/debian/rules
+++ b/debian/rules
@@ -21,7 +21,7 @@ CONFIGUREOPTS := --arch Linux --prefix /usr --mandir
/usr/share/man \
--with-doc no
configure: configure-stamp
-configure-stamp:
+configure-stamp: patch-stamp
dh_testdir
# git doesn't handle empty directories, so we create them here
-mkdir bin
@@ -34,7 +34,7 @@ configure-stamp:
touch configure-stamp
build: build-stamp
-build-stamp: patch-stamp configure-stamp
+build-stamp: configure-stamp
dh_testdir
if grep -q BEST=opt config/Makefile; \
then \
--
coq packaging
_______________________________________________
Pkg-ocaml-maint-commits mailing list
[email protected]
http://lists.alioth.debian.org/mailman/listinfo/pkg-ocaml-maint-commits
