diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-10-24 15:20:21 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-10-29 10:03:30 +0200 |
| commit | dfc6b66ec21e148d29b2a6e8b5d77873a0a47511 (patch) | |
| tree | e1b35810458543758dd5929b0546d81e9db7993c /driver/Clflags.ml | |
| parent | efc51afc7c8298ecd3b511b8d0faf9ff6d2df22e (diff) | |
| download | compcert-dfc6b66ec21e148d29b2a6e8b5d77873a0a47511.tar.gz compcert-dfc6b66ec21e148d29b2a6e8b5d77873a0a47511.zip | |
Unblock: never put debug info before a label
This ensures that normalized switch statements remain normalized.
However, if the label and the labeled statement are on different lines,
add an extra line directive corresponding to the label before the labeled
statement.
Diffstat (limited to 'driver/Clflags.ml')
0 files changed, 0 insertions, 0 deletions