From 624dc13d0e80dcde22beecd3c80e68037899c287 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 14 Jun 2017 18:58:03 +0200
Subject: [toplevel] Remove long ago deprecated and NOOP options.

Minor clean up, no sense in having these as they do nothing.
---
 tools/coqmktop.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'tools/coqmktop.ml')

diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 30e098df59..28a3c791cb 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 ->
-- 
cgit v1.2.3