diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-18 19:00:47 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-18 19:53:10 +0100 |
commit | 0a39cdab7f7ad8dc73339d17563a85d6f57f1710 (patch) | |
tree | 442514e22905ae3507e25dfed66fda9df7f56881 /cparser/GNUmakefile | |
parent | b3a52cf16ba3752797d983327f68a1199db9ba07 (diff) | |
download | compcert-0a39cdab7f7ad8dc73339d17563a85d6f57f1710.tar.gz compcert-0a39cdab7f7ad8dc73339d17563a85d6f57f1710.zip |
macOS: turn #warning off
The standard includes print irrelevant warnings using `#warning`.
The warnings can be restored by passing `-W#warning` to `ccomp`.
Diffstat (limited to 'cparser/GNUmakefile')
0 files changed, 0 insertions, 0 deletions