diff options
Diffstat (limited to 'arm/TargetPrinter.ml')
| -rw-r--r-- | arm/TargetPrinter.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 151326bb..9f435cee 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -157,6 +157,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Section_debug_loc -> ".section .debug_loc,\"\",%progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" + | Section_debug_line -> ".section .debug_ranges,\"\",%progbits" | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" let section oc sec = |