diff options
| author | Maxime Dénès | 2020-02-27 11:25:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-02-27 11:25:18 +0100 |
| commit | c160fc0da9bef60c4ee469cc2c35afd83fc16243 (patch) | |
| tree | 13714583d99546e125bf31d4347d08e8ea3838c1 /kernel/nativelib.mli | |
| parent | f97cb743386744e9da3ede4b6cf8c803c2f58fde (diff) | |
| parent | d8ee64ace969287dbec6ba2777c08f19a25cab26 (diff) | |
Merge PR #11581: [native compiler] Add options to set object directories.
Reviewed-by: gares
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/nativelib.mli')
| -rw-r--r-- | kernel/nativelib.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 52d18acca6..155fde54e9 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -13,7 +13,8 @@ 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 include_dirs : CUnix.physical_path list ref val get_load_paths : (unit -> string list) ref |