summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-18 15:52:05 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-19 15:18:13 +0200
commit6260e57c1e3a6bdbb9fc983ecbd7eecff433dcfa (patch)
tree37ea8397a6ae4fcc2f6f59c581909883e19f978b
parenta2630f381dd8cec31f0fe6ac603a29e5dcebf603 (diff)
Run test-suite in override_dh_auto_test, skip coqchk
-rwxr-xr-xdebian/rules4
1 files changed, 2 insertions, 2 deletions
diff --git a/debian/rules b/debian/rules
index fac32b76..ad1c70ea 100755
--- a/debian/rules
+++ b/debian/rules
@@ -49,7 +49,7 @@ ifeq ($(BUILDCACHE),)
# the default one without -silent (-silent maybe cause buildd to
# timeout because of lack of output)
- $(MAKE) STRIP=true VALIDOPTS="-o -m" COMPLEXITY= check
+ $(MAKE) world STRIP=true
$(MAKE) DOC_TARGETS=$(HTMLDOC) $(HTMLDOC)
else
rsync -a --exclude=debian --exclude=.git $(BUILDCACHE)/ .
@@ -57,7 +57,7 @@ endif
.PHONY: override_dh_auto_test
override_dh_auto_test:
-# TODO: run make check here instead of in override_dh_auto_build (?)
+ $(MAKE) check COMPLEXITY= BESTCHICKEN=/bin/true
.PHONY: override_dh_auto_install
override_dh_auto_install: