aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-03-14 05:14:07 +0100
committerEmilio Jesus Gallego Arias2019-03-28 00:56:23 +0100
commit392c8f87bac1e47e18a2d7929bd01c2097b9e43a (patch)
tree9cb5ce75d8cac6f10d5c0a9c73de4b2d14975666 /lib
parenta796822e5f57f74ff36e538fd2169f70a8c6c145 (diff)
[dune] Don't have `lib` depend on `dynlink`
This is convenient for the bootstrap of `coqdep`
Diffstat (limited to 'lib')
-rw-r--r--lib/dune2
-rw-r--r--lib/system.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/lib/dune b/lib/dune
index 8c6ef06e99..83783f9b5c 100644
--- a/lib/dune
+++ b/lib/dune
@@ -4,4 +4,4 @@
(public_name coq.lib)
(wrapped false)
(modules_without_implementation xml_datatype)
- (libraries dynlink coq.clib coq.config))
+ (libraries coq.clib coq.config))
diff --git a/lib/system.ml b/lib/system.ml
index fd6579dd69..c408061852 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -304,7 +304,7 @@ let with_time ~batch ~header f x =
raise e
(* We use argv.[0] as we don't want to resolve symlinks *)
-let get_toplevel_path ?(byte=not Dynlink.is_native) top =
+let get_toplevel_path ?(byte=Sys.(backend_type = Bytecode)) top =
let open Filename in
let dir = if String.equal (basename Sys.argv.(0)) Sys.argv.(0)
then "" else dirname Sys.argv.(0) ^ dir_sep in