From e11b3b885a6d359925b86743b89698cc6757157a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 27 Mar 2015 15:28:20 +0100
Subject: Updating the PowerPC and ARM ports. PowerPC: always use full register
 names to print annotations.

---
 powerpc/Asmexpand.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index c003bcd1..47895cb1 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -74,7 +74,7 @@ let _m8 = coqint_of_camlint (-8l)
 (* Handling of annotations *)
 
 let expand_annot_val txt targ args res =
-  emit (Pannot(EF_annot(txt, [AA_arg targ]), List.map (fun r -> APreg r) args));
+  emit (Pannot(EF_annot(txt, [targ]), List.map (fun r -> AA_base r) args));
   begin match args, res with
   | [IR src], [IR dst] ->
       if dst <> src then emit (Pmr(dst, src))
-- 
cgit