diff options
| author | Maxime Dénès | 2017-08-29 14:15:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-29 17:25:23 +0200 |
| commit | e581d018bfeaec2ffdf8697950eede5ce4282716 (patch) | |
| tree | 6e3e43d5f8909ab2b7085cbacdf32a1b64a94007 /test-suite | |
| parent | 799d17738ebbae30a007b308998a669a9139cf1d (diff) | |
Avoid running interactive tests on Windows.
This is a temporary workaround, until we fix the underlying issue which
makes coqtop hang on those tests.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 78d90aad81..ae426f0daf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -85,8 +85,10 @@ COMPLEXITY := $(if $(bogomips),complexity) BUGS := bugs/opened bugs/closed +INTERACTIVE := interactive + VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ - output-modulo-time interactive micromega $(COMPLEXITY) modules stm \ + output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ coqdoc # All subsystems |