diff options
| author | Emilio Jesus Gallego Arias | 2019-04-01 19:09:59 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-26 16:09:49 -0500 |
| commit | 9d52407e9fccf27d02d952d40f3758dfe1898767 (patch) | |
| tree | 904f2a306b616e23c381cebc3e930da4bf1246fb /kernel/nativelib.mli | |
| parent | f97cb743386744e9da3ede4b6cf8c803c2f58fde (diff) | |
[native compiler] Allow to set the output directory for cmx objects
This is useful in order to implement native support in Dune for
example, which as of today as strict target rules.
Hopefully this option could go away; it is really internal, but I've
chosen to document it.
Diffstat (limited to 'kernel/nativelib.mli')
| -rw-r--r-- | kernel/nativelib.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 52d18acca6..4d95f822e7 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -13,7 +13,7 @@ open Nativecode used by the native compiler. *) (* Directory where compiled files are stored *) -val output_dir : string +val output_dir : CUnix.physical_path ref val get_load_paths : (unit -> string list) ref |