diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-14 10:10:19 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-14 15:45:54 +0200 |
commit | ccfc5ced6a09ce2c8a1ebce81050c328c17c9bec (patch) | |
tree | 3412177948c85f853aef3996bebedc83c8100309 /backend/PrintLTLin.ml | |
parent | f5bb397acd12292f6b41438778f2df7391d6f2fe (diff) | |
download | compcert-ccfc5ced6a09ce2c8a1ebce81050c328c17c9bec.tar.gz compcert-ccfc5ced6a09ce2c8a1ebce81050c328c17c9bec.zip |
Reworked the section interface for the debug information.
Instead of pushing strings around use the actual section. However
the string is still used in the Hashtbl.
Bug 17392.
Diffstat (limited to 'backend/PrintLTLin.ml')
0 files changed, 0 insertions, 0 deletions