summaryrefslogtreecommitdiff
path: root/driver/Clflags.ml
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-11-01 16:51:47 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-11-01 16:51:47 +0000
commit3ccc93675292bf9a44ac0d7111d3f44981e1f56d (patch)
tree2879f37d1625e035f21134bc2307fce427531ce4 /driver/Clflags.ml
parent033aa0555a209fa3e825b1eeb8a5fc00ff8163e3 (diff)
Preliminary support for small data area in PowerPC port.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1163 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver/Clflags.ml')
-rw-r--r--driver/Clflags.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 08e4a53..81d4af3 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -17,6 +17,7 @@ let linker_options = ref ([]: string list)
let exe_name = ref "a.out"
let option_flonglong = ref false
let option_fmadd = ref false
+let option_fsda = ref false
let option_dclight = ref false
let option_dasm = ref false
let option_E = ref false