diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-02-03 19:16:03 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-02-03 19:16:03 +0100 |
| commit | fadf72ce0d252fc59890c1a2ffe95db14e4add88 (patch) | |
| tree | 49f52d0a91e205d212cddf64a4fb2b00a8351409 /driver | |
| parent | 0d6a1557ae45b8c731c6715bb7109a30c32c5a26 (diff) | |
| download | compcert-fadf72ce0d252fc59890c1a2ffe95db14e4add88.tar.gz compcert-fadf72ce0d252fc59890c1a2ffe95db14e4add88.zip | |
Added gcc cmd-line option -include.
The -include option is passed to the preprocessor and -include <file>
is equivalent to writting #include "<file>" as first line in the
primary source file.
Bug 18066.
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 81f28309..83078256 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -446,6 +446,8 @@ Preprocessing options: -D<symb>=<val> Define preprocessor symbol -U<symb> Undefine preprocessor symbol -Wp,<opt> Pass option <opt> to the preprocessor + -include <file> Process <file> as if #include \"<file>\" appears at the first + line of the primary source file. Language support options (use -fno-<opt> to turn off -f<opt>) : -fbitfields Emulate bit fields in structs [off] -flongdouble Treat 'long double' as 'double' [off] @@ -569,6 +571,7 @@ let cmdline_actions = Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options); Prefix "-Wp,", Self (fun s -> prepro_options := List.rev_append (explode_comma_option s) !prepro_options); + Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options); (* Language support options -- more below *) Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); |