diff options
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); \ |