diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 15:09:24 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 15:09:24 -0500 |
| commit | 4e783ae1e73875e34026baff95afc46351746098 (patch) | |
| tree | 9dce3b200a7a3a8bf195e3dcb6185fcfae028c10 /debian/patches/remove-bytecode-failing-tests.patch | |
| parent | 4f464870ea1f0f45abde3c10796b3f9268fbe757 (diff) | |
Fix build on platforms without ocamlopt
This includes disabling all unit tests, which require ocamlopt and
“don’t test much yet” anyway.
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 \ |