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 /extraction | |
parent | c8287e6578f313769c794fd407868b1ecb51c43f (diff) | |
download | compcert-7e71f5071b19415b4b285702e1753c9a82523acb.tar.gz compcert-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 'extraction')
0 files changed, 0 insertions, 0 deletions