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 /Makefile.menhir | |
| 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 'Makefile.menhir')
0 files changed, 0 insertions, 0 deletions