diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-08 15:17:43 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-11 20:43:00 +0100 |
| commit | 7d312541d49fd3eb8ed74ebcc2a6209014113c96 (patch) | |
| tree | 99bf1174ffd66ef1c62739f777732df046063efb /test-suite/Makefile | |
| parent | 3815ec5405976196ff79b6960e65ce5adda66205 (diff) | |
Fix undefined variables in test-suite/Makefile + add PRINT_LOGS
PRINT_LOGS can be used for interactive calls, eg
make report PRINT_LOGS=1
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index de669218c..16a56f440 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -40,6 +40,7 @@ coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source coqtopcompile := $(coqtop) -compile coqdep := $(BIN)coqdep -coqlib $(LIB) +VERBOSE?= SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) @@ -174,10 +175,20 @@ summary.log: # if not on travis we can get the log files (they're just there for a # local build, and downloadable on GitLab) +PRINT_LOGS?= +TRAVIS?= # special because we want to print travis_fold directives +ifdef APPVEYOR +PRINT_LOGS:=APPVEYOR +else +ifdef CIRCLECI +PRINT_LOGS:=CIRCLECI +endif #CIRCLECI +endif #APPVEYOR + report: summary.log $(HIDE)bash save-logs.sh $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi - $(HIDE)if [ "(" -n "${APPVEYOR}" ")" -o "(" -n "${CIRCLECI}" ")" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi + $(HIDE)if [ -n "${PRINT_LOGS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### |