diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/TargetPrinter.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 2e676090..b988f10f 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -157,7 +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_str -> ".section .debug_str,\"MS\",%progbits,1" let section oc sec = fprintf oc " %s\n" (name_of_section sec) |