From f758ce6d5de7cbfbf065587dbaf69ce28798e517 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 9 Dec 2004 13:48:01 +0000
Subject: 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
---
 test-suite/check | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

diff --git a/test-suite/check b/test-suite/check
index 5bc034aec7..838623ac0e 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"
-- 
cgit v1.2.3