diff options
Diffstat (limited to 'backend/PrintAnnot.ml')
| -rw-r--r-- | backend/PrintAnnot.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml index 54174b9f..26f96370 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -66,10 +66,10 @@ let print_file_line oc pref file line = | Some fb -> Printlines.copy oc pref fb line line end -(* Add file and line debug location, using DWARF1 directives in the style +(* Add file and line debug location, using DWARF2 directives in the style of Diab C 5 *) -let print_file_line_d1 oc pref file line = +let print_file_line_d2 oc pref file line = if !Clflags.option_g && file <> "" then begin let (_, filebuf) = try @@ -77,10 +77,10 @@ let print_file_line_d1 oc pref file line = with Not_found -> enter_filename file in if file <> !last_file then begin - fprintf oc " .d1file %S\n" file; + fprintf oc " .d2file %S\n" file; last_file := file end; - fprintf oc " .d1line %d\n" line; + fprintf oc " .d2line %d\n" line; match filebuf with | None -> () | Some fb -> Printlines.copy oc pref fb line line |