diff options
| author | Hugo Herbelin | 2020-04-12 14:46:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-12 14:46:41 +0200 |
| commit | 0d207dc4dc7d593c422ed81c07a7e1532899e4ec (patch) | |
| tree | 9e2d656e7c66dbf9c3e377a695312d3cab28114a /test-suite | |
| parent | afb4173e71f6069f7a49baf44b16569bf0cbcce4 (diff) | |
Exporting BEST as OPT for the tests using coq_makefile-generated Makefile.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index eade52b6eb..171b197891 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -62,6 +62,10 @@ coqtopbyte := $(BIN)coqtop.byte -q coqc_interactive := $(coqc) -test-mode -async-proofs-cache force coqdep := $(BIN)coqdep +# This is the convention for coq_makefile +OPT=-$(BEST) +export OPT + VERBOSE?= SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) |