diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-11-25 15:58:30 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-11-25 15:58:30 +0100 |
commit | 30959c8e41625ad158f71f55529ff1123ee23b9b (patch) | |
tree | 93ea1b85298441db515006a5ac377ec86970b6a9 /driver/Assembler.ml | |
parent | 40360396c621603af3ea6fb9a2fc89fa7945c79a (diff) | |
download | compcert-30959c8e41625ad158f71f55529ff1123ee23b9b.tar.gz compcert-30959c8e41625ad158f71f55529ff1123ee23b9b.zip |
Simplified diagnostics module.
Instead of constructing four different lists for maintaining the
state of the warnings only one list is now used. This list contains
the name of the warning and a boolean indicating whether this option
should be active by default. The rest is computed from this list.
Diffstat (limited to 'driver/Assembler.ml')
0 files changed, 0 insertions, 0 deletions