diff options
| -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) |