From f401437a97b09726d029e3a1b65143f34baaea70 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 24 Feb 2013 09:40:25 +0000
Subject: Updated ARM and PowerPC ports with new handling of __builtin_annot.
 ARM: add support for builtin_volatile_{read,write}_global, after all.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 ia32/PrintAsm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ia32')

diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 4f62640..4768606 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -231,9 +231,9 @@ let need_masks = ref false
 
 (* Handling of annotations *)
 
-let print_annot_stmt oc txt args =
+let print_annot_stmt oc txt targs args =
   fprintf oc "%s annotation: " comment;
-  PrintAnnot.print_annot_stmt preg "ESP" oc txt args
+  PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args
 
 let print_annot_val oc txt args res =
   fprintf oc "%s annotation: " comment;
-- 
cgit v1.2.3