aboutsummaryrefslogtreecommitdiffstats
path: root/myocamlbuild.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2014-09-30 13:10:26 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2014-09-30 13:10:26 +0200
commita2bed030e01bfe6e3addbe44f724de5c5fbeab65 (patch)
treeaeffd4bcba1743dd5fdcc08e2f2e9f51962e4402 /myocamlbuild.ml
parente5b59af8a21c42b504b1beeb89208dd0cb0c8b3b (diff)
downloadcompcert-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 'myocamlbuild.ml')
0 files changed, 0 insertions, 0 deletions