aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile.build4
-rw-r--r--configure.ml2
2 files changed, 1 insertions, 5 deletions
diff --git a/Makefile.build b/Makefile.build
index 5b26f11b12..e5cff50c86 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -269,10 +269,6 @@ OPT:=
BESTOBJ:=.cmo
BESTLIB:=.cma
BESTDYN:=.cma
-
-# needed while booting if non -local
-CAML_LD_LIBRARY_PATH := $(PWD)/kernel/byterun:$(CAML_LD_LIBRARY_PATH)
-export CAML_LD_LIBRARY_PATH
endif
define bestobj
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 ()