diff options
| author | Enrico Tassi | 2019-05-29 13:09:07 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-29 13:09:07 +0200 |
| commit | d47b279c2b0510535ef6f1affe23c7fab812c745 (patch) | |
| tree | 473977a856b5bb3273fda348775c39a4cb3f78b1 /test-suite/Makefile | |
| parent | d62215a4c06680d2052238544b9e31422f512eaf (diff) | |
| parent | 356f496f16219c5e3bd9a651b867c48411bde17d (diff) | |
Merge PR #10270: Fix debug printers
Reviewed-by: gares
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); \ |