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/Commandline.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/Commandline.ml')
| -rw-r--r-- | driver/Commandline.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/driver/Commandline.ml b/driver/Commandline.ml index 0a2c8fca..1981776e 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -16,6 +16,7 @@ (* Parsing of command-line flags and arguments *) open Printf +open Responsefile type pattern = | Exact of string @@ -99,4 +100,9 @@ let parse_array spec argv first last = in parse first let parse_cmdline spec = - parse_array spec Sys.argv 1 (Array.length Sys.argv - 1) + try + let argv = expand_responsefiles Sys.argv in + parse_array spec argv 1 (Array.length argv - 1) + with Arg.Bad s -> + eprintf "%s" s; + exit 2 |