summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorThomas Bauereiss2020-03-27 18:06:26 +0000
committerThomas Bauereiss2020-04-10 13:22:11 +0100
commit550db27f8c27e03ecc4defc804c8f360af64fbd6 (patch)
treedfd9f8145b98934cd5d695c8d733c3caf830bace /test
parent0207a2ce56250a1d277871dc2ed546aab5255e3a (diff)
Update path for newer versions of BBV Coq library
Diffstat (limited to 'test')
-rwxr-xr-xtest/coq/run_tests.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh
index db73580f..da6bce69 100755
--- a/test/coq/run_tests.sh
+++ b/test/coq/run_tests.sh
@@ -5,7 +5,7 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
SAILDIR="$DIR/../.."
TYPECHECKTESTSDIR="$DIR/../typecheck/pass"
EXTRATESTSDIR="$DIR/pass"
-BBVDIR="$DIR/../../../bbv/theories"
+BBVDIR="$DIR/../../../bbv/src/bbv"
RED='\033[0;31m'
GREEN='\033[0;32m'