diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-26 10:18:58 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-26 10:18:58 +0200 |
commit | 0c00ace3c8981516ef02bc49f4e616e4cb485124 (patch) | |
tree | f5600124386717114332368893aa521c36e7f0ca /backend/PrintLTLin.ml | |
parent | cc264a58d6fb43cf7c8ae41d73726dfedc20f1d4 (diff) | |
download | compcert-0c00ace3c8981516ef02bc49f4e616e4cb485124.tar.gz compcert-0c00ace3c8981516ef02bc49f4e616e4cb485124.zip |
Also quote \a.
This allows for an easier replacement of the binary address and
avoids that the user specifies his own binary addresses.
Bug 22468
Diffstat (limited to 'backend/PrintLTLin.ml')
0 files changed, 0 insertions, 0 deletions