From 95f751136ba3a8f8c2544d8d7d48125c52030836 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 10 Oct 2018 13:34:44 +0200
Subject: [test-suite] Don't reset `OCAMLPATH`, but append to it.

This fixes an obvious bug introduced in #8602.
---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index b4cc3dda11..168a662fd7 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -254,7 +254,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 # otherwise the directory name will include the quotes, see
 # see for example https://stackoverflow.com/questions/10424645/how-to-convert-a-quoted-string-to-a-normal-one-in-makefile
 ifeq ($(LOCAL),true)
-  export OCAMLPATH := $(shell echo $(COQLIBINSTALL))
+  export OCAMLPATH := $(shell echo $(COQLIBINSTALL):$$OCAMLPATH)
 endif
 
 OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
-- 
cgit v1.2.3