diff options
Diffstat (limited to 'debian/patches/remove-bytecode-failing-tests.patch')
| -rw-r--r-- | debian/patches/remove-bytecode-failing-tests.patch | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/debian/patches/remove-bytecode-failing-tests.patch b/debian/patches/remove-bytecode-failing-tests.patch new file mode 100644 index 00000000..49fe7fc3 --- /dev/null +++ b/debian/patches/remove-bytecode-failing-tests.patch @@ -0,0 +1,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 \ |