From 400f852347be1b038369878df997bf537ff1f3d0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 10 Nov 2020 14:24:34 +0100
Subject: Fix running unit tests with dune compiled coq

(for runs outside dune, ie "make -C test-suite unit-tests" rather than
"dune build @runtest")

Fix #13333
---
 test-suite/Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6c373701cf..279f32c903 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -36,7 +36,8 @@ include ../Makefile.common
 # Note that this will later need an eval in shell to interpret the quotes
 ROOT='$(shell cd ..; pwd)'
 
-ifneq ($(wildcard ../_build),)
+ifneq ($(wildcard ../_build/default/config/Makefile),)
+include ../_build/default/config/Makefile
 BIN:=$(ROOT)/_build/install/default/bin/
 # COQLIB is an env variable so no quotes
 COQLIB:=$(shell cd ..; pwd)/_build/install/default/lib/coq
-- 
cgit v1.2.3