diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 16:49:08 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 16:49:08 -0500 |
| commit | 4bf1d996c98a37c312c5dddf418316d77086e9c2 (patch) | |
| tree | 891c5d766bb1a36dff2f11657dec5a30af684729 | |
| parent | 7cbefd56ba087ae51bc618db5bc72a51d10dedbf (diff) | |
Disable .vio tests, as they don’t work on bytecode architectures
Operations with .vio files fail when Coq has been compiled with ocamlc;
see https://github.com/coq/coq/issues/9141. Disable tests related
to .vio generation to prevent this from breaking the build.
| -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 \ |