summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorJon French2018-10-16 16:25:39 +0100
committerJon French2018-10-16 17:03:30 +0100
commit315fccb1b063f5ffa131b5a761fa1b2d33fa130f (patch)
treeeed4db4a25e3c1c44d7394f4749ef1612c7af105 /test
parent45ce9105ce90efeccb9d0a183390027cdb1536af (diff)
parent58c1292f2f5a54f069e00e4065c00936963db8cd (diff)
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'test')
-rwxr-xr-xtest/coq/run_tests.sh3
1 files changed, 2 insertions, 1 deletions
diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh
index 5a723a06..db73580f 100755
--- a/test/coq/run_tests.sh
+++ b/test/coq/run_tests.sh
@@ -56,7 +56,8 @@ function check_tests_dir {
do
if $SAILDIR/sail -coq -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null;
then
- if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v out.v &>/dev/null;
+ if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v &>/dev/null &&
+ coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out.v &>/dev/null;
then
green "tested $i expecting pass" "pass"
else