diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-04-23 18:40:56 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-04-23 18:40:56 +0200 |
| commit | 1a52f581eb9cc52e5c1862c7e73253016109e1fc (patch) | |
| tree | ec4fd781aa06fc80c0c00a9a0f4cc2190c99177f /driver | |
| parent | bb5dab84859088d70074444cfbf0e51f14e3c782 (diff) | |
| download | compcert-kvx-1a52f581eb9cc52e5c1862c7e73253016109e1fc.tar.gz compcert-kvx-1a52f581eb9cc52e5c1862c7e73253016109e1fc.zip | |
Remove `-version-file` option from option summary
The `-version-file` option was removed in commit 600803cae, but remained
in the option summary, as reported in #386.
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/CommonOptions.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index e8a6941c..a816dd41 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -77,7 +77,6 @@ let general_help = -v Print external commands before invoking them -timings Show the time spent in various compiler passes -version Print the version string and exit - -version-file <file> Print version inforation to <file> and exit -target <value> Generate code for the given target -conf <file> Read configuration from file @<file> Read command line options from <file> |