aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rwxr-xr-xtest-suite/check12
1 files changed, 10 insertions, 2 deletions
diff --git a/test-suite/check b/test-suite/check
index e4fd2a4c9..47960e98d 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