diff options
Diffstat (limited to 'ia32')
-rw-r--r-- | ia32/PrintAsm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 4f626405..4768606c 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; |