diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-03-20 13:12:16 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-03-20 13:12:16 +0100 |
commit | 361253d66fde0eb79d3fde7cc272e43689768ee7 (patch) | |
tree | c7defd7e8e935a341677e54ee40f1c1a50feb650 /backend/Regalloc.ml | |
parent | 5bfa0059a144fb4333bbfecaa74690ba92a879ce (diff) | |
download | compcert-361253d66fde0eb79d3fde7cc272e43689768ee7.tar.gz compcert-361253d66fde0eb79d3fde7cc272e43689768ee7.zip |
Better fix for problems with quoting in files.
Instead of using Filename.quote, string entries are printed with
%S.
Bug 21216
Diffstat (limited to 'backend/Regalloc.ml')
0 files changed, 0 insertions, 0 deletions