diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-09 09:50:35 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-09 09:50:35 +0100 |
| commit | d50509fb3a74cae6c5851eeff2b54fba5cfd425c (patch) | |
| tree | 2ba6ca7322b66fb24b87fe2c09a20176568781a3 /backend/Fileinfo.ml | |
| parent | 5063ae307001dcddbfcc60e7abda04cf98bffeb4 (diff) | |
| download | compcert-d50509fb3a74cae6c5851eeff2b54fba5cfd425c.tar.gz compcert-d50509fb3a74cae6c5851eeff2b54fba5cfd425c.zip | |
Do not use default printer for variable names.
Printing variable names with the default expression printer
results in newlines in the outputed error message.
Bug 23169
Diffstat (limited to 'backend/Fileinfo.ml')
0 files changed, 0 insertions, 0 deletions