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