aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-12-09 13:48:01 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-12-09 13:48:01 +0000
commitf758ce6d5de7cbfbf065587dbaf69ce28798e517 (patch)
tree5bc5e8c254a88d6ebb483a513769481d384b857e
parent7d78cf9acda678659064a12af5cdd31430b7fc3c (diff)
Réactivation des tests output avec test aussi de la nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6452 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xtest-suite/check20
1 files changed, 17 insertions, 3 deletions
diff --git a/test-suite/check b/test-suite/check
index 5bc034aec..838623ac0 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -86,6 +86,21 @@ test_output() {
echo "Error! (unexpected output)"
fi
done
+ for f in $1/*.v8; do
+ nbtests=`expr $nbtests + 1`
+ printf " "$f"..."
+ cp $f tmp8.v
+ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
+ $command tmp8.v 2>&1 | tail +3 > $tmpoutput
+ foutput=`dirname $f`/`basename $f .v8`.out8
+ if [ $? = 0 ]; then
+ echo "Ok"
+ nbtestsok=`expr $nbtestsok + 1`
+ else
+ echo "V8 Error! (unexpected output)"
+ fi
+ rm tmp8.v
+ done
}
# La fonction suivante teste l'analyseur syntaxique fournit par "parser"
@@ -112,9 +127,8 @@ test_parser() {
# Programme principal
-# echo "Output tests"
-# test_output output
-echo "[Output tests are off]"
+echo "Output tests"
+test_output output
echo "Success tests"
test_success success
echo "Failure tests"