diff options
Diffstat (limited to 'debug/DwarfUtil.ml')
-rw-r--r-- | debug/DwarfUtil.ml | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml index e2c87a9d..d5e72adb 100644 --- a/debug/DwarfUtil.ml +++ b/debug/DwarfUtil.ml @@ -14,18 +14,8 @@ open DwarfTypes -let id = ref 0 - -let next_id () = - let nid = !id in - incr id; nid - -let reset_id () = - id := 0 - (* Generate a new entry from a given tag *) -let new_entry tag = - let id = next_id () in +let new_entry id tag = { tag = tag; children = []; |