diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-03-21 15:46:43 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-03-24 11:59:58 +0100 |
| commit | b6b5aae1d406c200035ff7400de46eed2d88fd85 (patch) | |
| tree | 8990b00fcf497fb35aadc7631b2fe94f225410c5 /Makefile.extr | |
| parent | 8827f9bc5d68726bc04a4cd8d26321868bd76b7f (diff) | |
| download | compcert-b6b5aae1d406c200035ff7400de46eed2d88fd85.tar.gz compcert-b6b5aae1d406c200035ff7400de46eed2d88fd85.zip | |
Do not emit line info before case stmt.
Since before a case statement is potentially unreachable code due
to break, etc. it is better to skip printing line information
directly before the case statement and print it afterwards.
Bug 21232
Diffstat (limited to 'Makefile.extr')
0 files changed, 0 insertions, 0 deletions