diff options
Diffstat (limited to 'debug')
-rw-r--r-- | debug/DwarfUtil.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml index ec5495c1..100e35bf 100644 --- a/debug/DwarfUtil.ml +++ b/debug/DwarfUtil.ml @@ -26,6 +26,10 @@ let reset_id () = (* Hashtable to from type name to entry id *) let type_table: (string, int) Hashtbl.t = Hashtbl.create 7 +(* Clear the type map *) +let reset_type_table () = + Hashtbl.clear type_table + (* Generate a new entry from a given tag *) let new_entry tag = let id = next_id () in @@ -35,7 +39,6 @@ let new_entry tag = id = id; } - (* Add an entry as child to another entry *) let add_children entry child = {entry with children = child::entry.children;} |