From 0d207dc4dc7d593c422ed81c07a7e1532899e4ec Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Apr 2020 14:46:41 +0200
Subject: Exporting BEST as OPT for the tests using coq_makefile-generated
 Makefile.

---
 test-suite/Makefile | 4 ++++
 1 file changed, 4 insertions(+)

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),,@)
-- 
cgit v1.2.3