diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-07-28 11:48:45 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-07-28 13:37:57 +0200 |
| commit | db0c2d0f86e7fb2153be13431641a2fad0babf90 (patch) | |
| tree | 21270b3d0a0fc8ed2394068fd32b98cc27a2469c | |
| parent | 8dd1802846b1f7a2304c7e63b2cf907d70f14fe1 (diff) | |
patch-stamp and configure-stamp are dependencies of build-stamp
This is needed for proper parallel build (-j option of
dpkg-buildpackage). However, check target of Coq Makefile doesn't
handle well parallel build yet (will be fixed in next version).
| -rwxr-xr-x | debian/rules | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/debian/rules b/debian/rules index 8ae84589..1dc43f97 100755 --- a/debian/rules +++ b/debian/rules @@ -28,8 +28,8 @@ configure-stamp: fi touch configure-stamp -build: patch-stamp configure-stamp build-stamp -build-stamp: +build: build-stamp +build-stamp: patch-stamp configure-stamp dh_testdir if grep -q BEST=opt config/Makefile; \ then \ |