diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-04 19:10:26 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2022-09-23 13:55:44 +0200 |
| commit | 32910495644e7f6fbf9b3b85ecc16f4e30447e60 (patch) | |
| tree | 81109ee811c3cf76c26b4741fee587133cee301e /debug/DebugInit.ml | |
| parent | 9785a3cc148ad93dba1ea153f3390d6aab514755 (diff) | |
| download | compcert-32910495644e7f6fbf9b3b85ecc16f4e30447e60.tar.gz compcert-32910495644e7f6fbf9b3b85ecc16f4e30447e60.zip | |
Export the functions that control warnings
Activation and deactivation of a given warning,
plus set-as-error and remove-as-error.
Diffstat (limited to 'debug/DebugInit.ml')
0 files changed, 0 insertions, 0 deletions