aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorglondu2008-09-07 00:10:49 +0000
committerglondu2008-09-07 00:10:49 +0000
commit7217f11ef754f58bb86eafeb4f0daeaee7647b7f (patch)
tree4878f2548f07469697d20c62e2a76d8ab5acb49c
parenta5e035d42a7043bcafe392c8e964ce85558cd319 (diff)
Skip complexity tests on demand
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11375 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xtest-suite/check12
1 files changed, 10 insertions, 2 deletions
diff --git a/test-suite/check b/test-suite/check
index e4fd2a4c95..47960e98d5 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -250,8 +250,16 @@ echo "Interactive tests"
test_interactive interactive
echo "Micromega tests"
test_success micromega
-echo "Complexity tests"
-test_complexity complexity
+
+# We give a chance to disable the complexity tests which may cause
+# random build failures on build farms
+if [ -z "$COQTEST_SKIPCOMPLEXITY" ]; then
+ echo "Complexity tests"
+ test_complexity complexity
+else
+ echo "Skipping complexity tests"
+fi
+
echo "Module tests"
$coqtop -compile modules/Nat
$coqtop -compile modules/plik