diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-10-18 16:32:56 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-10-18 16:32:56 +0200 |
| commit | 5975b2e5568b5b32e42153d281017660de155e27 (patch) | |
| tree | e3dc68da4cdc1211ff8c62f82aa1993b90b029da /driver | |
| parent | ab6a906f09514d1ed81fb0970fb7151021407062 (diff) | |
| download | compcert-5975b2e5568b5b32e42153d281017660de155e27.tar.gz compcert-5975b2e5568b5b32e42153d281017660de155e27.zip | |
Document -target and -conf. Bug 20210
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 739ba9b4..a273a91a 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -331,6 +331,8 @@ 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\ +\ -target <value> Generate code for the given target\n\ +\ -conf <file> Read configuration from file\n\ \ @<file> Read command line options from <file>\n" ^ Cerrors.warning_help ^ "Interpreter mode:\n\ |