diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-11 13:30:26 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-11 13:30:26 +0100 |
commit | e1b0d579d7c0971856a3ada74078e51b3797a30a (patch) | |
tree | 6cb6fd057b9c526a53dfbd607b466351ffe7563c /arm/TargetPrinter.ml | |
parent | 7b0ce5abd6a31a3790dfcfd3be69064bd5ca5eb3 (diff) | |
download | compcert-e1b0d579d7c0971856a3ada74078e51b3797a30a.tar.gz compcert-e1b0d579d7c0971856a3ada74078e51b3797a30a.zip |
Add a target option.
This option allows it to specify a .ini file that is in the usual
search path.
Bug 17431
Diffstat (limited to 'arm/TargetPrinter.ml')
0 files changed, 0 insertions, 0 deletions