diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-08-24 17:23:02 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-08-24 17:23:02 +0200 |
commit | 95ed4ea7df3e4b05d623afb9cb65f0eb2653361b (patch) | |
tree | 70eb5be48918a9b857df429cfa479dde4d2d1d23 | |
parent | 2c0518a387cb0d79faae3c4545ab4eb2317665dd (diff) | |
download | compcert-95ed4ea7df3e4b05d623afb9cb65f0eb2653361b.tar.gz compcert-95ed4ea7df3e4b05d623afb9cb65f0eb2653361b.zip |
Document -finline in help.
-rw-r--r-- | driver/Driver.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index dfbac67f..45a5c769 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -255,6 +255,7 @@ Processing options: (<n>=0: none, <n>=1: limited, <n>=2: full; default is full) -fcse Perform common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] + -finline Perform inlining of functions [on] Code generation options: (use -fno-<opt> to turn off -f<opt>) -ffpu Use FP registers for some integer operations [on] -fsmall-data <n> Set maximal size <n> for allocation in small data area |