diff options
| author | Gaëtan Gilbert | 2019-05-28 17:25:58 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-28 18:49:03 +0200 |
| commit | 356f496f16219c5e3bd9a651b867c48411bde17d (patch) | |
| tree | d559813a8e7a00effa672dea7b5df9d70a199f43 /test-suite/Makefile | |
| parent | be21788fc5cbe86af52d4f0ea21daa73ed8fcf4f (diff) | |
Fix printers.sh test when missing coqtop.byte, print more info
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 94011447d7..552d007f85 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -561,7 +561,6 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) export coqc="$(coqc)"; \ export coqtop="$(coqc)"; \ export coqdep="$(coqdep)"; \ - export coqtopbyte="$(coqtopbyte)"; \ "$<" 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ |