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 /powerpc/Op.v | |
parent | eea30300a784da4516b67e38024587af11ba2100 (diff) | |
download | compcert-da76ba512d1efbae8ab5ebcb79eb58c0085a026b.tar.gz compcert-da76ba512d1efbae8ab5ebcb79eb58c0085a026b.zip |
bug 23325, document recently introduced named warnings
Diffstat (limited to 'powerpc/Op.v')
0 files changed, 0 insertions, 0 deletions