diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 10:12:16 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 10:12:16 +0100 |
| commit | cb1da9d8176ea397b833f56ee49af5c75338676f (patch) | |
| tree | 0a4437025f77dbc3197063fe242ccd25bcb481c0 /ia32 | |
| parent | fcd5ba10674f499d4e270bfb68fa40da8857fb47 (diff) | |
| download | compcert-cb1da9d8176ea397b833f56ee49af5c75338676f.tar.gz compcert-cb1da9d8176ea397b833f56ee49af5c75338676f.zip | |
Removed unused sel_target, changed cygwin symbol names and changed the default function aligment to be target dependent.
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/TargetPrinter.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 55abe3b7..39f8be23 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -82,8 +82,9 @@ module Cygwin_System : SYSTEM = let raw_symbol oc s = fprintf oc "_%s" s - - let symbol = elf_symbol + + let symbol oc symb = + raw_symbol oc (extern_atom symb) let label oc lbl = fprintf oc "L%d" lbl @@ -179,7 +180,7 @@ module MacOS_System : SYSTEM = fprintf oc "_%s" s let symbol oc symb = - fprintf oc "_%s" (extern_atom symb) + raw_symbol oc (extern_atom symb) let label oc lbl = fprintf oc "L%d" lbl @@ -967,6 +968,8 @@ module Target(System: SYSTEM):TARGET = System.print_epilogue oc let comment = comment + + let default_falignment = 16 end let sel_target () = |