diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-19 14:47:01 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-19 14:47:01 +0100 |
| commit | 7e71f5071b19415b4b285702e1753c9a82523acb (patch) | |
| tree | d6e1b4c29d3e8b3543329a81657ffddb514f0c2c /Makefile.extr | |
| parent | c8287e6578f313769c794fd407868b1ecb51c43f (diff) | |
| download | compcert-kvx-7e71f5071b19415b4b285702e1753c9a82523acb.tar.gz compcert-kvx-7e71f5071b19415b4b285702e1753c9a82523acb.zip | |
Use Unix.create_process instead of Sys.command to run external tools.
Revised parsing of compcert.ini file to split arguments into words
like POSIX shell does (including quotes).
Diffstat (limited to 'Makefile.extr')
0 files changed, 0 insertions, 0 deletions