summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rwxr-xr-xtest/coq/run_tests.sh6
1 files changed, 4 insertions, 2 deletions
diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh
index c31b1475..2d1a1318 100755
--- a/test/coq/run_tests.sh
+++ b/test/coq/run_tests.sh
@@ -6,10 +6,12 @@ SAILDIR="$DIR/../.."
TYPECHECKTESTSDIR="$DIR/../typecheck/pass"
EXTRATESTSDIR="$DIR/pass"
-if [ -z "$BBVDIR" ] || opam config var coq-bbv:share >/dev/null 2>/dev/null; then
+if opam config var coq-bbv:share >/dev/null 2>/dev/null; then
COQOPTS="-Q $SAILDIR/lib/coq Sail"
else
- BBVDIR="$DIR/../../../bbv/src/bbv"
+ if [ -z "$BBVDIR" ]; then
+ BBVDIR="$DIR/../../../bbv/src/bbv"
+ fi
COQOPTS="-Q $SAILDIR/lib/coq Sail -Q $BBVDIR bbv"
fi