diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-07-11 12:49:52 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-07-11 12:49:52 +0000 |
commit | 28e9b3e7b8237c99f8f395d8edd8cb1dbe8c183c (patch) | |
tree | 6234ee4f842fd117350b3a7d886e2b90651391f0 /caml | |
parent | db185cc89cd2e731eff80ec2276bf43584d83120 (diff) | |
download | compcert-28e9b3e7b8237c99f8f395d8edd8cb1dbe8c183c.tar.gz compcert-28e9b3e7b8237c99f8f395d8edd8cb1dbe8c183c.zip |
Declaration des variables avec .comm
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@50 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml')
-rw-r--r-- | caml/PrintPPC.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml index b9eb7286..830de0d5 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -326,9 +326,7 @@ let print_function oc (Coq_pair(name, code)) = coqlist_iter (print_instruction oc (labels_of_code code)) code let print_var oc (Coq_pair(name, size)) = - fprintf oc " .globl %a\n" print_symb name; - fprintf oc "%a:\n" print_symb name; - fprintf oc " .space %ld\n" (camlint_of_z size) + fprintf oc " .comm %a, %ld\n" print_symb name (camlint_of_z size) let print_program oc p = coqlist_iter (print_var oc) p.prog_vars; |