diff options
Diffstat (limited to 'ia32')
-rw-r--r-- | ia32/PrintAsm.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index e6f905a3..b42f4314 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -80,8 +80,8 @@ module Cygwin_System = let raw_symbol oc s = fprintf oc "_%s" s - let symbol oc symb = - fprintf oc "%s" (extern_atom symb) + let symbol oc s = + raw_symbol oc (extern_atom symb) let label oc lbl = fprintf oc "L%d" lbl @@ -177,9 +177,9 @@ module ELF_System = let raw_symbol oc s = fprintf oc "%s" s - - let symbol oc symb = - fprintf oc "%s" (extern_atom symb) + + let symbol oc s = + raw_symbol oc (extern_atom symb) let label oc lbl = fprintf oc ".L%d" lbl @@ -231,8 +231,8 @@ module MacOS_System = let raw_symbol oc s = fprintf oc "_%s" s - let symbol oc symb = - fprintf oc "_%s" (extern_atom symb) + let symbol oc s = + raw_symbol oc (extern_atom symb) let label oc lbl = fprintf oc "L%d" lbl |