diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-01 11:05:15 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-01 11:05:15 +0200 |
commit | 18859319b1daee0abb32bbc4e89ec5865a6fe082 (patch) | |
tree | d50056bf5867a7d6b0144a098b18f929e2b90888 /Makefile.extr | |
parent | 0eba6f63b6bc458d856e477f6f8ec6b78ef78c58 (diff) | |
download | compcert-18859319b1daee0abb32bbc4e89ec5865a6fe082.tar.gz compcert-18859319b1daee0abb32bbc4e89ec5865a6fe082.zip |
clightgen -short-idents : do not use $"xxx" notation ever
In the original code, collisions could occur: an identifier could
be numbered with a number that happens to be equal to its canonical
encoding. This was harmless but confusing.
Closes: #358
Diffstat (limited to 'Makefile.extr')
0 files changed, 0 insertions, 0 deletions