diff options
Diffstat (limited to 'debug/DwarfUtil.ml')
| -rw-r--r-- | debug/DwarfUtil.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml index 764194a6..91ef94a8 100644 --- a/debug/DwarfUtil.ml +++ b/debug/DwarfUtil.ml @@ -33,10 +33,15 @@ let new_entry tag = } (* Add an entry as child to another entry *) -let add_children entry child = +let add_child entry child = {entry with children = child::entry.children;} +(* Add entries as children to another entry *) +let add_children entry children = + {entry with children = entry.children@children;} + + let list_iter_with_next f list = let rec aux = (function | [] -> () |