summaryrefslogtreecommitdiff
path: root/kernel/nativelibrary.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /kernel/nativelibrary.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'kernel/nativelibrary.ml')
-rw-r--r--kernel/nativelibrary.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 0b8662ff..443cd8c2 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -62,12 +62,12 @@ let dump_library mp dp env mod_expr =
let prefix = mod_uid_of_dirpath dp ^ "." in
let t0 = Sys.time () in
clear_global_tbl ();
- clear_symb_tbl ();
+ clear_symbols ();
let mlcode =
List.fold_left (translate_field prefix mp env) [] struc
in
let t1 = Sys.time () in
let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
let mlcode = add_header_comment (List.rev mlcode) time_info in
- mlcode, get_symbols_tbl ()
+ mlcode, get_symbols ()
| _ -> assert false