From db1719fbac08b5582fafddd4b76ef92f69cc5bc1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 28 Feb 2018 03:26:12 +0100
Subject: [ide] Remove special option `-ideslave`

This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
---
 toplevel/coqargs.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 5c1ffd784..89602c9b5 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -529,7 +529,6 @@ let parse_args arglist : coq_cmdopts * string list =
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
     |"-filteropts" -> { oval with filter_opts = true }
-    |"-ideslave" -> Flags.ide_slave := true; oval
     |"-impredicative-set" ->
       { oval with impredicative_set = Declarations.ImpredicativeSet }
     |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval
-- 
cgit v1.2.3