diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-07 13:00:04 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-07 13:00:04 +0100 |
commit | 0386265191303ca71d054e5f868d2a9e92f30fc5 (patch) | |
tree | 9c31c5ae0028c4a01aa4bf2b8af287a064544fca /cparser/Cleanup.ml | |
parent | a0ce43e04778660a6f0ec98e70d7b54c5c987fcb (diff) | |
download | compcert-0386265191303ca71d054e5f868d2a9e92f30fc5.tar.gz compcert-0386265191303ca71d054e5f868d2a9e92f30fc5.zip |
Ignore *.cmt(i) files and allow global COMPFLAGS.
Instead of using = to set the COMPFLAGS use += which allows it to
specify custom compiler flags in for example the Makefile.config.
Also remove *.cmt(i) files and add them to the .gitignore file.
Bug 17742
Diffstat (limited to 'cparser/Cleanup.ml')
0 files changed, 0 insertions, 0 deletions