diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-11 13:30:26 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-11 13:30:26 +0100 |
| commit | e1b0d579d7c0971856a3ada74078e51b3797a30a (patch) | |
| tree | 6cb6fd057b9c526a53dfbd607b466351ffe7563c /driver/Driver.ml | |
| parent | 7b0ce5abd6a31a3790dfcfd3be69064bd5ca5eb3 (diff) | |
| download | compcert-e1b0d579d7c0971856a3ada74078e51b3797a30a.tar.gz compcert-e1b0d579d7c0971856a3ada74078e51b3797a30a.zip | |
Add a target option.
This option allows it to specify a .ini file that is in the usual
search path.
Bug 17431
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 8d144ad5..c9c16eac 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -572,7 +572,8 @@ let cmdline_actions = Exact "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n); Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n); (* Target processor options *) - Exact "--conf", String (fun _ -> ()); (* Ignore option since it is already handled *) + Exact "-conf", String (fun _ -> ()); (* Ignore option since it is already handled *) + Exact "-target", String (fun _ -> ()); (* Ignore option since it is already handled *) Exact "-mthumb", Set option_mthumb; Exact "-marm", Unset option_mthumb; (* Assembling options *) |