diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-09-30 13:10:26 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-09-30 13:10:26 +0200 |
commit | a2bed030e01bfe6e3addbe44f724de5c5fbeab65 (patch) | |
tree | aeffd4bcba1743dd5fdcc08e2f2e9f51962e4402 /driver/Driver.ml | |
parent | e5b59af8a21c42b504b1beeb89208dd0cb0c8b3b (diff) | |
download | compcert-a2bed030e01bfe6e3addbe44f724de5c5fbeab65.tar.gz compcert-a2bed030e01bfe6e3addbe44f724de5c5fbeab65.zip |
Change the way the tools like the linker, assembler, etc. are specified by including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
Diffstat (limited to 'driver/Driver.ml')
0 files changed, 0 insertions, 0 deletions