diff options
| author | Enrico Tassi | 2018-10-10 18:09:38 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-10-10 18:09:38 +0200 |
| commit | 040ad198e38776bb9f398329243b2fe41434f2d5 (patch) | |
| tree | 51547819395d4f6798a9c2368c85fb521e820657 | |
| parent | ea38cc10b1b3d81e2346de6b95076733ef4fd7bb (diff) | |
| parent | 95f751136ba3a8f8c2544d8d7d48125c52030836 (diff) | |
Merge PR #8692: [test-suite] Don't reset `OCAMLPATH`, but append to it.
| -rw-r--r-- | test-suite/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
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) |