1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sun, 11 Aug 2019 18:33:24 +0200
Subject: Disable tests which require ocamlopt
MIME-Version: 1.0
Content-Type: text/plain; charset="utf-8"
Content-Transfer-Encoding: 8bit
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.
---
test-suite/Makefile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
--- coq.orig/test-suite/coq-makefile/findlib-package-unpacked/run.sh
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/usr/bin/bash
-
-. ../template/init.sh
-mv src/test_plugin.mlpack src/test_plugin.mllib
-sed -i.old 's/rocq-runtime.plugins.ltac/rocq-runtime.plugins.ltac,foo/' src/META.coq-test-suite
-
-echo "let () = Foolib.foo ();;" >> src/test_aux.ml
-if which cygpath 2>/dev/null; then
- # separator is ; on windows
- OCAMLPATH=$OCAMLPATH;$(cygpath -m "$PWD"/findlib)
-else
- OCAMLPATH=$OCAMLPATH:$PWD/findlib
-fi
-make -C findlib/foo clean
-rocq makefile -f _CoqProject -o Makefile
-cat Makefile.conf
-cat Makefile.local
-make -C findlib/foo
-if which ocamlopt >/dev/null 2>&1; then
- make
-fi
-make byte
|
