diff options
| author | Maxime Dénès | 2017-08-30 13:47:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-30 13:47:31 +0200 |
| commit | bdaf7032912feabf5ee97af33bf32e4359ad2d25 (patch) | |
| tree | edc516f6a3cafebc8c924e385b012b32af56de6c | |
| parent | 21462199ad335f44aa74f3746f805b2694eba650 (diff) | |
| parent | e581d018bfeaec2ffdf8697950eede5ce4282716 (diff) | |
Merge PR #998: Avoid running interactive tests on Windows.
| -rw-r--r-- | appveyor.yml | 3 | ||||
| -rw-r--r-- | test-suite/Makefile | 4 |
2 files changed, 5 insertions, 2 deletions
diff --git a/appveyor.yml b/appveyor.yml index ec6ded7218..fb5a445848 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -23,4 +23,5 @@ build_script: - cmd: '%CYGROOT%/bin/bash -lc "cd $APPVEYOR_BUILD_FOLDER && ./configure -local && make"' test_script: -- cmd: '%CYGROOT%/bin/bash -lc "cd $APPVEYOR_BUILD_FOLDER && make -C test-suite && make validate"' +- cmd: '%CYGROOT%/bin/bash -lc "cd $APPVEYOR_BUILD_FOLDER && make -C test-suite all + INTERACTIVE= && make validate"' 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 |