diff options
Diffstat (limited to 'tools/dumpobj.ml')
| -rw-r--r-- | tools/dumpobj.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/dumpobj.ml b/tools/dumpobj.ml index db8494cc26..f1255e9cd2 100644 --- a/tools/dumpobj.ml +++ b/tools/dumpobj.ml @@ -493,6 +493,7 @@ let dump_obj filename ic = if cu.cu_debug > 0 then begin seek_in ic cu.cu_debug; let evl = (input_value ic : debug_event list) in + ignore (input_value ic); (* Skip the list of absolute directory names *) record_events 0 evl end; seek_in ic cu.cu_pos; @@ -531,6 +532,7 @@ let dump_exe ic = for _i = 1 to num_eventlists do let orig = input_binary_int ic in let evl = (input_value ic : debug_event list) in + ignore (input_value ic); (* Skip the list of absolute directory names *) record_events orig evl done with Not_found -> () |