From 4e783ae1e73875e34026baff95afc46351746098 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Tue, 5 Feb 2019 15:09:24 -0500 Subject: Fix build on platforms without ocamlopt MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This includes disabling all unit tests, which require ocamlopt and “don’t test much yet” anyway. --- debian/patches/remove-bytecode-failing-tests.patch | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 debian/patches/remove-bytecode-failing-tests.patch (limited to 'debian/patches/remove-bytecode-failing-tests.patch') 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 +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 \ -- cgit v1.2.3