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 /debian/patches/fix-bytecode-build.patch | |
| 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.
Diffstat (limited to 'debian/patches/fix-bytecode-build.patch')
0 files changed, 0 insertions, 0 deletions