diff options
| author | Vincent Laporte | 2018-10-11 12:23:35 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-11 12:23:35 +0000 |
| commit | 96b30e352ff30b1fba4f11b278f22aa6db5871f9 (patch) | |
| tree | ee4d38ec56aa6343f99d933abb98e175e3d89a01 | |
| parent | 4a244648cff78c7f7333ac5b335de3f6e742908a (diff) | |
| parent | f9020057455ba4863ef62826b3548b44e3497367 (diff) | |
Merge PR #8709: [test-suite] Use the right OCAMLPATH separator on Windows.
| -rw-r--r-- | test-suite/Makefile | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 168a662fd7..928a77cb8e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -250,11 +250,19 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v # Unit tests ####################################################################### +# An alternative is ifeq ($(OS),Windows_NT) using make's own variable. +ifeq ($(ARCH),win32) + export FINDLIB_SEP=";" +else + export FINDLIB_SEP=":" +endif + # COQLIBINSTALL is quoted in config/make thus we must unquote it, # 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):$$OCAMLPATH) + export OCAMLPATH := $(shell echo $(COQLIBINSTALL)$(FINDLIB_SEP)$$OCAMLPATH) endif OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) |