diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-28 03:26:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-21 03:07:27 +0200 |
| commit | db1719fbac08b5582fafddd4b76ef92f69cc5bc1 (patch) | |
| tree | a88bf6867103dbf87d701cc2e2205e67b5f4e7d0 /toplevel | |
| parent | 382ee49700c4b4ee78ba95b2e86866ebd3b35d74 (diff) | |
[ide] Remove special option `-ideslave`
This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 1 |
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 |