diff options
| -rw-r--r-- | backend/PrintAsmaux.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 07ab4bed..0db664ce 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -200,9 +200,11 @@ let annot_text preg_string sp_reg_name txt args = let ais_annot_list: (int * Str.split_result list) list ref = ref [] let re_annot_addr = Str.regexp "%addr" +let re_annot_quote = Str.regexp "\007" let ais_annot_text lbl preg_string sp_reg_name txt args = let annot = annot_text preg_string sp_reg_name txt args in + let annot = Str.global_replace re_annot_quote "\007\000" annot in let annots = Str.full_split re_annot_addr annot in ais_annot_list := (lbl,annots)::!ais_annot_list; annot |