From 9b98d49bbc105d998f9a63868d4b23bfab8d4cf7 Mon Sep 17 00:00:00 2001
From: Michael Schmidt <github@mschmidt.me>
Date: Fri, 15 Dec 2017 12:20:49 +0100
Subject: Reintroduce informative comment for Ploadsymbol_lbl in target printer

---
 arm/TargetPrinter.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'arm/TargetPrinter.ml')

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index bb7f24df..d402b4a8 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -515,8 +515,8 @@ struct
        fprintf oc "	vmov.f32 %a, #%.15F\n"
          freg_single r1 (Int32.float_of_bits f)
     | Ploadsymbol_lbl (r1,lbl,id,ofs) ->
-      fprintf oc "	ldr	%a, %a\n"
-        ireg r1 print_label lbl
+      fprintf oc "	ldr	%a, %a %s %a\n"
+        ireg r1 print_label lbl comment symbol_offset (id, ofs)
 
 
   let get_section_names name =
-- 
cgit