diff options
| author | Pierre-Marie Pédrot | 2015-07-18 12:18:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-18 12:18:05 +0200 |
| commit | 88e2da8c1b9403f5eac19df4f6c55fedca948bcc (patch) | |
| tree | 01f750142359361f800e0dc2dfe422f145f491c5 /kernel/nativelibrary.mli | |
| parent | 139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (diff) | |
| parent | fdd6a17b272995237c9f95fc465bb1ff6871bedc (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'kernel/nativelibrary.mli')
| -rw-r--r-- | kernel/nativelibrary.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index a66fb715d9..29368d1408 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -14,4 +14,4 @@ open Nativecode compiler *) val dump_library : module_path -> dir_path -> env -> module_signature -> - global list * symbol array + global list * symbols |