aboutsummaryrefslogtreecommitdiffstats
path: root/arm/TargetPrinter.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-10-15 09:10:22 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-10-15 09:10:22 +0200
commit44845982f412810b0c18067987f2780ef6245fbb (patch)
tree9ca5afb4851a726229251415d977abf296f68f5e /arm/TargetPrinter.ml
parentdf78560fdf859644274dbdabccdd1fdb9e75634e (diff)
downloadcompcert-kvx-44845982f412810b0c18067987f2780ef6245fbb.tar.gz
compcert-kvx-44845982f412810b0c18067987f2780ef6245fbb.zip
Use section type also for other targets.
Bug 17392.
Diffstat (limited to 'arm/TargetPrinter.ml')
-rw-r--r--arm/TargetPrinter.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 4961f897..3bffe59b 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -902,7 +902,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
if !Clflags.option_g then begin
section oc Section_text;
let low_pc = new_label () in
- Debug.add_compilation_section_start ".text" low_pc;
+ Debug.add_compilation_section_start Section_text low_pc;
fprintf oc "%a:\n" elf_label low_pc;
fprintf oc " .cfi_sections .debug_frame\n"
end
@@ -911,7 +911,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
let print_epilogue oc =
if !Clflags.option_g then begin
let high_pc = new_label () in
- Debug.add_compilation_section_end ".text" high_pc;
+ Debug.add_compilation_section_end Section_text high_pc;
Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
section oc Section_text;
fprintf oc "%a:\n" elf_label high_pc