From 5332a2c2b3e7d8d41dd40c75ff44496bb9c25c8f Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 24 Mar 2004 18:12:52 +0000
Subject: bug de PP des fix (coqbugs #574)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5550 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/check | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite/check')

diff --git a/test-suite/check b/test-suite/check
index 65c4197ebd..1c7822d104 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -39,6 +39,19 @@ test_success() {
 	    echo "V7 Error! (should be accepted)"
         fi 
     done
+    for f in $1/*.v8; do 
+	nbtests=`expr $nbtests + 1`
+	printf "    "$f"..."
+        cp $f tmp8.v
+	$command tmp8.v > /dev/null 2>&1
+        if [ $? = 0 ]; then
+            echo "Ok"
+            nbtestsok=`expr $nbtestsok + 1`
+        else
+            echo "V8 Error! (should be accepted)"
+        fi
+        rm tmp8.v
+    done
 }
 
 # La fonction suivante teste le compilateur sur des fichiers qu'il doit
-- 
cgit v1.2.3