aboutsummaryrefslogtreecommitdiff
path: root/configure.ml
diff options
context:
space:
mode:
authorHugo Herbelin2020-04-12 14:45:16 +0200
committerHugo Herbelin2020-04-12 14:45:16 +0200
commitafb4173e71f6069f7a49baf44b16569bf0cbcce4 (patch)
tree57ca7ed03205069b7122d2d4a1cfd5179f079f48 /configure.ml
parent227520b14e978e19d58368de873521a283aecedd (diff)
Fixing export of CAML_LD_LIBRARY_PATH from config/Makefile to Makefile.common.
There were single quotes which were not interpreted in "PATH" syntax.
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index eaa0e321b0..282b40db27 100644
--- a/configure.ml
+++ b/configure.ml
@@ -983,7 +983,7 @@ let config_runtime () =
["-dllib";"-lcoqrun";"-dllpath";("\"" ^ coqtop ^ "/kernel/byterun\"")]
| _ ->
let ld="CAML_LD_LIBRARY_PATH" in
- build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld;
+ build_loadpath := sprintf "export %s:=%s/kernel/byterun:$(%s)" ld coqtop ld;
["-dllib";"-lcoqrun";"-dllpath";coqlib/"kernel/byterun"]
let vmbyteflags = config_runtime ()