diff options
Diffstat (limited to 'kernel/nativecode.mli')
| -rw-r--r-- | kernel/nativecode.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 9e35dbd1b..5d8ae96f0 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -44,6 +44,8 @@ type code_location_update type code_location_updates type linkable_code = global list * code_location_updates +val clear_global_tbl : unit -> unit + val empty_updates : code_location_updates val register_native_file : string -> unit |