aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-12-17 14:51:31 +0100
committerGaëtan Gilbert2018-12-17 14:51:31 +0100
commit76d64fc2df0ddeb08e5ef0661ceee9fdba1da3b1 (patch)
tree162792d1ba0b8c1a7a6396fc1e2042d4243aded6 /test-suite
parent854d3e1b404fb3ee9087ffb07cbba7cc9196c1f9 (diff)
parent85b91b71abe7e60a9096ae31b9d0b4afda2189bb (diff)
Merge PR #8856: [gitlab] Test Ocaml trunk.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile12
-rw-r--r--test-suite/dune2
2 files changed, 8 insertions, 6 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 530671e1a1..34a1900bbc 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -90,19 +90,17 @@ FAIL = >&2 echo 'FAILED $@'
# Testing subsystems
#######################################################################
-# Apart so that it can be easily skipped with overriding
+# These targets can be skipped by doing `make TARGET= test-suite`
COMPLEXITY := $(if $(bogomips),complexity)
-
BUGS := bugs/opened bugs/closed
-
INTERACTIVE := interactive
-
+UNIT_TESTS := unit-tests
VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
coqdoc ssr
# All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools unit-tests
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
PREREQUISITELOG = prerequisite/admit.v.log \
prerequisite/make_local.v.log prerequisite/make_notation.v.log \
@@ -119,6 +117,10 @@ PREREQUISITELOG = prerequisite/admit.v.log \
all: run
$(MAKE) report
+# do nothing
+.PHONY: noop
+noop: ;
+
run: $(SUBSYSTEMS)
bugs: $(BUGS)
diff --git a/test-suite/dune b/test-suite/dune
index c5fa0bb14a..eae072553a 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -70,4 +70,4 @@
(progn
; XXX: we will allow to set the NJOBS variable in a future Dune
; version, either by using an env var or by letting Dune set `-j`
- (run make -j 2 BIN= PRINT_LOGS=1))))
+ (run make -j 2 BIN= PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}))))