diff options
Diffstat (limited to 'backend/PrintAsm.ml')
| -rw-r--r-- | backend/PrintAsm.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index a6883339..a394cf8e 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -15,6 +15,7 @@ open AST open Asm open Camlcoq open Datatypes +open DwarfPrinter open PrintAsmaux open Printf open Sections @@ -98,4 +99,9 @@ let print_program oc p = Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; Target.print_epilogue oc; - PrintAnnot.close_filenames () + PrintAnnot.close_filenames (); + if !Clflags.option_g && Configuration.advanced_debug then + begin + let module DebugPrinter = DwarfPrinter(Target) in + () + end |