diff options
| author | Théo Zimmermann | 2019-03-28 08:54:25 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-28 08:54:25 +0100 |
| commit | 383bcf46b12799762fefec7e06fe00b5e33f5a18 (patch) | |
| tree | 02f610e7c5de11820ce0409dfb6c574b91012bbc /lib | |
| parent | 21e9d207a8d8a0bee74c000f02a4e2819c53fae5 (diff) | |
| parent | 392c8f87bac1e47e18a2d7929bd01c2097b9e43a (diff) | |
Merge PR #9850: [dune] Don't have `lib` depend on `dynlink`
Reviewed-by: Zimmi48
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/dune | 2 | ||||
| -rw-r--r-- | lib/system.ml | 2 |
2 files changed, 2 insertions, 2 deletions
@@ -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 |
