blob: 49fe7fc3c752148f7372b5296272aaf46224baec (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
From: Benjamin Barenblat <bbaren@debian.org>
Subject: Disable tests which require ocamlopt
Forwarded: not-needed
Disable unit tests. They require ocamlopt, which isn't available on all
Debian architectures, and Gaëtan Gilbert says that "they don't test much
yet" anyway.
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -102,7 +102,7 @@
coqdoc
# 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
PREREQUISITELOG = prerequisite/admit.v.log \
prerequisite/make_local.v.log prerequisite/make_notation.v.log \
|
