aboutsummaryrefslogtreecommitdiffstats
path: root/ci
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2020-01-16 12:16:42 +0100
committerChantal Keller <Chantal.Keller@lri.fr>2020-01-16 12:16:42 +0100
commit2e7f2df3955cb0714af19d971dadc353547bc11a (patch)
tree42e3a4fa03515a9da5d920c33421bda3a9671e6e /ci
parent90d3ce10b41159c0bfe266ce403e4b5f31d970cf (diff)
downloadsmtcoq-2e7f2df3955cb0714af19d971dadc353547bc11a.tar.gz
smtcoq-2e7f2df3955cb0714af19d971dadc353547bc11a.zip
Fix CI manifest
Diffstat (limited to 'ci')
-rw-r--r--ci/manifest5
1 files changed, 4 insertions, 1 deletions
diff --git a/ci/manifest b/ci/manifest
index 33d9f6d..b002ce3 100644
--- a/ci/manifest
+++ b/ci/manifest
@@ -36,9 +36,12 @@ tasks:
cd bin
ln -s ~/cvc4-1.6-x86_64-linux-opt cvc4
ln -s ~/veriT9f48a98/veriT veriT
-- test: |
+- unit: |
eval $(opam env)
export PATH=~/bin:$PATH
+ export LFSCSIGS="/home/build/smtcoq/src/lfsc/tests/signatures/"
+ export DONTSHOWVERIT="yes"
cd smtcoq/unit-tests
+ sed -i "s/..\/src/~\/.opam\/ocaml-base-compiler.4.09.0\/lib\/coq\/user-contrib\/SMTCoq/g" Makefile
make verit
make lfsc