From 3b0cdb49d0bc602820bd0667a735aa92bca9cece Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 2 Dec 2008 22:37:24 +0000
Subject: Add new directory for pre-compilation of files needed for further
 tests. Application to the test of notation import from within a section.

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

(limited to 'test-suite/check')

diff --git a/test-suite/check b/test-suite/check
index 47960e98d5..68a4b0e384 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -9,6 +9,7 @@ else
 fi
 
 command="$coqtop -top Top -load-vernac-source"
+coqc="$coqtop -compile"
 
 # on compte le nombre de tests et de succès
 nbtests=0
@@ -234,8 +235,24 @@ test_features () {
     done
 }
 
+# Compile in advance files needed for tests involving a "Require"
+prepare_tests () {
+    files=`/bin/ls -1 $1/*.v 2> /dev/null`
+    for f in $files; do 
+	printf "    "$f"..."
+	$coqc $1/`basename $f .v` > /dev/null 2>&1 
+	if [ $? != 0 ]; then
+	    echo "could not be prepared"
+        else 
+	    echo "correctly prepared"
+        fi
+    done
+}
+
 # Programme principal
 
+echo "Preparing tests"
+prepare_tests prerequisite
 echo "Success tests"
 test_success success
 echo "Failure tests"
-- 
cgit v1.2.3