aboutsummaryrefslogtreecommitdiff
path: root/test-suite/Makefile
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-12-19 14:18:12 +0100
committerGaëtan Gilbert2019-12-19 14:18:12 +0100
commitec505a2fa67b0776b624be54417e06c6512f1734 (patch)
treeeabba8073654087361d24ec50a71e12dc8bf35b8 /test-suite/Makefile
parent6621e7cf79d7d824461de14007b2a06cabe59aef (diff)
Fix #11303: skip complexity tests on windows even if bogomips found
Apparently the bogomips produced by cygwin are extra-bogo.
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile4
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 609a61226b..bcaac9752e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -71,6 +71,9 @@ get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_
get_set_impredicativity= $(filter "-impredicative-set",$(call get_coq_prog_args,$(1)))
bogomips:=
+ifeq (win32,$(ARCH))
+ $(warning windows detected: skipping complexity tests)
+else
ifneq (,$(wildcard /proc/cpuinfo))
sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc
sedbogo += -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" # sparc
@@ -81,6 +84,7 @@ endif
ifeq (,$(bogomips))
$(warning cannot run complexity tests (no bogomips found))
endif
+endif
# keep these synced with test-suite/save-logs.sh
log_success = "==========> SUCCESS <=========="