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