aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqargs.ml1
1 files changed, 0 insertions, 1 deletions
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