diff options
| author | coqbot-app[bot] | 2020-11-10 23:09:05 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-10 23:09:05 +0000 |
| commit | af42e1bec2df12355725bc79e2060f5d3acd0ce1 (patch) | |
| tree | 9ab7cd52c832c7d8e27b35e69aedebcccc21f581 | |
| parent | 417e8c513e4372bcd622603912cfb2d9f1069619 (diff) | |
| parent | 400f852347be1b038369878df997bf537ff1f3d0 (diff) | |
Merge PR #13335: Fix running unit tests with dune compiled coq
Reviewed-by: ejgallego
| -rw-r--r-- | test-suite/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
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 |