diff options
author | François Pottier <francois.pottier@inria.fr> | 2015-11-03 10:32:55 +0100 |
---|---|---|
committer | François Pottier <francois.pottier@inria.fr> | 2015-11-03 10:32:55 +0100 |
commit | 2ca1282f84c5da41328b1251ac7bbcfa417b9be6 (patch) | |
tree | 6be3904b9b50c1a44d26b827dc16db2aa2529f2a /cfrontend/PrintCsyntax.ml | |
parent | fe73ed58ef80da7c53c124302a608948fb190229 (diff) | |
download | compcert-2ca1282f84c5da41328b1251ac7bbcfa417b9be6.tar.gz compcert-2ca1282f84c5da41328b1251ac7bbcfa417b9be6.zip |
When printing a fragment of source text as part of an error message, compress multiple whitespace characters into just one space character.
This is done before the call to [sanitize], which replaces special characters with a dot.
This produces more a readable result when the error spans multiple lines.
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
0 files changed, 0 insertions, 0 deletions