Fix "unknown option '-no-keep-docs'" (#765)

There was a typo in this option name.
2016-08-18 12:30:10 +02:00 · 2016-08-18 12:30:10 +02:00 · b0aa84b647
parent 7bd6587180
commit b0aa84b647
1 changed files with 1 additions and 1 deletions
--- a/driver/main_args.ml
+++ b/driver/main_args.ml
@ -228,7 +228,7 @@ let mk_keep_docs f =
 ;;

 let mk_no_keep_docs f =
-  "-keep-docs", Arg.Unit f,
+  "-no-keep-docs", Arg.Unit f,
  " Do not keep documentation strings in .cmi files (default)"
 ;;