diff options
Diffstat (limited to 'tools/coqmktop.ml')
| -rw-r--r-- | tools/coqmktop.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 30e098df5..28a3c791c 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -175,8 +175,6 @@ let parse_args () = | "-top" :: rem -> top := true ; parse (op,fl) rem | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem | "-echo" :: rem -> echo := true ; parse (op,fl) rem - | ("-v8"|"-full" as o) :: rem -> - Printf.eprintf "warning: option %s deprecated\n" o; parse (op,fl) rem (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *) | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem -> |