aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Readconfig.mll
Commit message (Collapse)AuthorAgeFilesLines
* bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-141-2/+2
|
* Use Unix.create_process instead of Sys.command to run external tools.Xavier Leroy2014-12-191-0/+111
Revised parsing of compcert.ini file to split arguments into words like POSIX shell does (including quotes).