diff options
author | 2018-03-31 18:47:52 +0200 | |
---|---|---|
committer | 2018-05-16 02:26:03 +0200 | |
commit | a2e34cd42ef6a4327e701416114c6b8b85a173d6 (patch) | |
tree | 69850e82ea83b7f3327b59fcd9257e9dae643ef8 /ide/coq_commands.mli | |
parent | acdb3608cb1faf18826981ba2fecd8e7781e5e4b (diff) |
[ide] Don't set `quiet` on start.
This makes `coqidetop` behavior consistent with the one of
`coqtop`.
This was likely needed in the past when Coq used to print all kind of
stuff to stdout, including goal display. Now, it is not the case
anymore and this flag mainly controls printing verbosity.
Diffstat (limited to 'ide/coq_commands.mli')
0 files changed, 0 insertions, 0 deletions