diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-31 18:47:52 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-16 02:26:03 +0200 |
commit | a2e34cd42ef6a4327e701416114c6b8b85a173d6 (patch) | |
tree | 69850e82ea83b7f3327b59fcd9257e9dae643ef8 /doc/tools/coqrst/repl/coqtop.py | |
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 'doc/tools/coqrst/repl/coqtop.py')
0 files changed, 0 insertions, 0 deletions