diff options
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 32e245e36..33b402327 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -519,6 +519,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ + export BIN="$(BIN)"; \ export coqc="$(coqc)"; \ export coqtop="$(coqtop)"; \ export coqdep="$(coqdep)"; \ |