aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelib.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativelib.mli')
-rw-r--r--kernel/nativelib.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index a262a9f58..b74d4fdd0 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -21,7 +21,7 @@ val get_ml_filename : unit -> string * string
val compile : string -> global list -> profile:bool -> bool * string
-val compile_library : Names.dir_path -> global list -> string -> bool
+val compile_library : Names.DirPath.t -> global list -> string -> bool
val call_linker :
?fatal:bool -> string -> string -> code_location_updates option -> unit