diff options
-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> |