summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 15:21:57 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-01-03 18:25:04 -0500
commit3a01cbe3fca2e9e1ab6ad056804770ebcb496a06 (patch)
tree51894d9ab043b140c4f7118773ea5f3edba9c8e5
parent6fabd6380fd08b6e3defdfceb137b47d4db858a3 (diff)
Don't run testsuite under nocheck build profile
-rwxr-xr-xdebian/rules2
1 files changed, 2 insertions, 0 deletions
diff --git a/debian/rules b/debian/rules
index db2ddc0f..55cd0491 100755
--- a/debian/rules
+++ b/debian/rules
@@ -82,8 +82,10 @@ endif
.PHONY: override_dh_auto_test
override_dh_auto_test:
+ifeq (,$(filter nocheck,$(DEB_BUILD_OPTIONS)))
CAML_LD_LIBRARY_PATH=$PWD/kernel/byterun COQLIB=$PWD \
$(MAKE) test-suite COMPLEXITY=
+endif
.PHONY: override_dh_auto_install
override_dh_auto_install: