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 /Makefile.menhir | |
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 'Makefile.menhir')
0 files changed, 0 insertions, 0 deletions