diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-08 10:15:31 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-08 10:15:31 +0200 |
| commit | ea2d6b70ed06c60dba9ba81cf53883c85fb92068 (patch) | |
| tree | d0ac3273943f124a59cd3f20aaa007589929a700 /driver/Driver.ml | |
| parent | db2445b3b745abd1a26f5a832a29ca269c725277 (diff) | |
| download | compcert-ea2d6b70ed06c60dba9ba81cf53883c85fb92068.tar.gz compcert-ea2d6b70ed06c60dba9ba81cf53883c85fb92068.zip | |
Added responsefile support for commandline.
Commandline can now be passed in a file specifed with @file on the
Commandline. The quoting convention is similar to the one used by
gcc, etc. Options are separated by whitespaces and options with
whitespaecs need to be quoted.
Bug 18303
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 7311215d..6d8cf9ac 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -334,6 +334,7 @@ General options:\n\ \ -v Print external commands before invoking them\n\ \ -timings Show the time spent in various compiler passes\n\ \ -version Print the version string and exit\n\ +\ @<file> Read command line options from <file>\n\ Interpreter mode:\n\ \ -interp Execute given .c files using the reference interpreter\n\ \ -quiet Suppress diagnostic messages for the interpreter\n\ |