diff options
Diffstat (limited to 'debian/patches/remove-bytecode-failing-tests.patch')
| -rw-r--r-- | debian/patches/remove-bytecode-failing-tests.patch | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/debian/patches/remove-bytecode-failing-tests.patch b/debian/patches/remove-bytecode-failing-tests.patch index 49fe7fc3..393ae940 100644 --- a/debian/patches/remove-bytecode-failing-tests.patch +++ b/debian/patches/remove-bytecode-failing-tests.patch @@ -5,6 +5,9 @@ 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. + +Also disable .vio tests, as they run afoul +of https://github.com/coq/coq/issues/9141. --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -102,7 +102,7 @@ @@ -12,7 +15,7 @@ yet" anyway. # 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 ++SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide coqchk coqwc coq-makefile tools PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log \ |