summaryrefslogtreecommitdiff
path: root/debian/rules
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-05 12:53:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-05 12:53:14 +0200
commit581c27825b108d2a0ab9ee8e068bde947ede8ddd (patch)
treea4952ddb2151334c909f66988ca828c81457c54b /debian/rules
parentd43a92cbe2dd9b90393698e98eb96104b14c04fa (diff)
Call coqchk without -silentdebian/8.2.pl1+dfsg-2
Diffstat (limited to 'debian/rules')
-rwxr-xr-xdebian/rules8
1 files changed, 7 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules
index 014134a7..0dcf678e 100755
--- a/debian/rules
+++ b/debian/rules
@@ -44,8 +44,14 @@ configure-stamp: ocamlinit-stamp
build: build-stamp
build-stamp: configure-stamp
dh_testdir
+
ifeq ($(BUILDCACHE),)
- $(MAKE) STRIP=true check
+
+# VALIDOPTS are the options given to coqchk; the value given here is
+# the default one without -silent (-silent maybe cause buildd to
+# timeout because of lack of output)
+
+ $(MAKE) STRIP=true VALIDOPTS="-o -m" check
$(MAKE) DOC_TARGETS=$(HTMLDOC) $(HTMLDOC)
else
rsync -a --exclude=debian --exclude=.git $(BUILDCACHE)/ .