aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/check
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-09-21 14:24:16 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-09-21 14:24:16 +0000
commit69f4e481e14477454a15844e18e760c8623ffe3a (patch)
treef24246a07b18588b6acfedd90523571a40aeb74b /test-suite/check
parent9632f263fe29c90c42d6e18979e6b2466a92430f (diff)
Correction d'un bug dans check + ajout de tests
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10134 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/check')
-rwxr-xr-xtest-suite/check4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/check b/test-suite/check
index b8577dee4..dd51c1e76 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -198,7 +198,7 @@ test_bugs () {
# At last, we test closed bugs that should fail
- files=`/bin/ls -1 $1/bugs/closed/shouldfail/*.v 2> /dev/null`
+ files=`/bin/ls -1 $1/closed/shouldfail/*.v 2> /dev/null`
for f in $files; do
nbtests=`expr $nbtests + 1`
printf " "$f"..."
@@ -207,7 +207,7 @@ test_bugs () {
echo "Ok"
nbtestsok=`expr $nbtestsok + 1`
else
- echo "Error! (bug seems to be opend, please check)"
+ echo "Error! (bug seems to be opened, please check)"
fi
done