diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-31 15:56:09 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-31 16:25:56 +0200 |
| commit | 7c1b6714fe73c6cd8685bccef58eb6839a57fcb9 (patch) | |
| tree | ae5b1ef3301c64ca031f0391ba730cf03fafc07b /test-suite/Makefile | |
| parent | 6b4a57051a470436b50d53e7395ec44b52e2dc7e (diff) | |
[travis] print failing test suite logs on failure
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 285460762..cc635dd13 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -68,6 +68,7 @@ ifeq (,$(bogomips)) $(warning cannot run complexity tests (no bogomips found)) endif +# keep these synced with test-suite/save-logs.sh log_success = "==========> SUCCESS <==========" log_segfault = "==========> FAILURE <==========" log_anomaly = "==========> FAILURE <==========" @@ -164,7 +165,13 @@ summary.log: $(SHOW) BUILDING SUMMARY FILE $(HIDE)$(MAKE) --quiet summary > "$@" +# if not on travis we can get the log files (they're just there for a +# local build, and downloadable on GitLab) report: summary.log + $(HIDE)./save-logs.sh + $(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:start:coq.logs'; fi + $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec cat '{}' ';'; fi + $(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:end:coq.logs'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### |