diff options
Diffstat (limited to 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index f9ed569f..7e075f04 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -289,12 +289,20 @@ let print_inline_asm print_preg oc txt sg args res = let print_version_and_options oc comment = let version_string = if Version.buildnr <> "" && Version.tag <> "" then - sprintf "%s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag + sprintf "Release: %s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag else Version.version in fprintf oc "%s File generated by CompCert %s\n" comment version_string; fprintf oc "%s Command line:" comment; - for i = 1 to Array.length Sys.argv - 1 do - fprintf oc " %s" Sys.argv.(i) + for i = 1 to Array.length Commandline.argv - 1 do + fprintf oc " %s" Commandline.argv.(i) done; fprintf oc "\n" +(** Get the name of the common section if it is used otherwise the given section + name, with bss as default *) + +let common_section ?(sec = ".bss") () = + if !Clflags.option_fcommon then + "COMM" + else + sec |