aboutsummaryrefslogtreecommitdiffstats
path: root/runtime
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-03-09 09:50:35 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2018-03-09 09:50:35 +0100
commitd50509fb3a74cae6c5851eeff2b54fba5cfd425c (patch)
tree2ba6ca7322b66fb24b87fe2c09a20176568781a3 /runtime
parent5063ae307001dcddbfcc60e7abda04cf98bffeb4 (diff)
downloadcompcert-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 'runtime')
0 files changed, 0 insertions, 0 deletions