diff options
| author | Michael Schmidt <github@mschmidt.me> | 2018-06-05 12:55:11 +0200 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2018-06-05 12:55:11 +0200 |
| commit | da76ba512d1efbae8ab5ebcb79eb58c0085a026b (patch) | |
| tree | cb185a112e4ccf0e98abb7ed784e7744c67866ec /Makefile | |
| parent | eea30300a784da4516b67e38024587af11ba2100 (diff) | |
| download | compcert-da76ba512d1efbae8ab5ebcb79eb58c0085a026b.tar.gz compcert-da76ba512d1efbae8ab5ebcb79eb58c0085a026b.zip | |
bug 23325, document recently introduced named warnings
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions