From 9b8f0f6c4683dd00ee0e3422b84c9cc34510011e Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 1 Jul 2012 07:40:04 +0000
Subject: Added option -falign-functions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 ia32/PrintAsm.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'ia32')

diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index ccc3c0f..096e1e3 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -737,7 +737,9 @@ let print_function oc name code =
     | [t;l;j] -> (t, l, j)
     |    _    -> (Section_text, Section_literal, Section_jumptable) in
   section oc text;
-  print_align oc 16;
+  let alignment =
+    match !Clflags.option_falignfunctions with Some n -> n | None -> 16 in
+  print_align oc alignment;
   if not (C2C.atom_is_static name) then
     fprintf oc "	.globl %a\n" symbol name;
   fprintf oc "%a:\n" symbol name;
-- 
cgit v1.2.3