From e22bb9841a5186d0b52b8fa9ad8cf2e46fa51d76 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Sun, 14 Jun 2020 22:27:30 +0100
Subject: Coq: tidy up scope in library Helps with Coq 8.11.  Also fix BBVDIR
 default in test script.

---
 test/coq/run_tests.sh | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'test')

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
 
-- 
cgit v1.2.3