summaryrefslogtreecommitdiff
path: root/debian
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-18 22:32:05 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-18 22:32:05 +0000
commit39a05ea8ddf4411a5abd7ef804bd5d40ee8f3bda (patch)
tree40bcde75f180ef968e8794a19f3d25982c63c942 /debian
parent1aa163f8f8c548e69b94188497b72a5c1242edb1 (diff)
We only need to call check since world depends on it.
Diffstat (limited to 'debian')
-rwxr-xr-xdebian/rules15
1 files changed, 6 insertions, 9 deletions
diff --git a/debian/rules b/debian/rules
index 62c14ed8..be9ce98e 100755
--- a/debian/rules
+++ b/debian/rules
@@ -25,29 +25,26 @@ configure-stamp: patch
build: patch-stamp configure-stamp build-stamp
build-stamp:
dh_testdir
+ touch test-suite/success/debian.v8
if grep -q BEST=opt config/Makefile; \
then \
- echo opt > best-stamp; \
- $(MAKE) world \
+ $(MAKE) check \
|| (echo WARNING: NATIVE CODE COMPILATION FAILED \
&& echo Trying to build coq in bytecode instead \
- && echo byte > best-stamp \
&& $(MAKE) archclean clean \
- && $(MAKE) BEST=byte world \
+ && touch test-suite/success/debian.v8 \
+ && $(MAKE) BEST=byte check \
&& echo NATIVE CODE COMPILATION FAILED \
&& echo Coq was built in bytecode instead); \
else \
- echo byte > best-stamp; \
- $(MAKE) world; \
+ $(MAKE) check; \
fi
- touch test-suite/success/debian.v8
- $(MAKE) BEST=`cat best-stamp` check
touch build-stamp
clean: unpatch
dh_testdir
dh_testroot
- rm -f build-stamp configure-stamp best-stamp
+ rm -f build-stamp configure-stamp
-$(MAKE) clean
-$(MAKE) archclean