aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-31 18:47:52 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-16 02:26:03 +0200
commita2e34cd42ef6a4327e701416114c6b8b85a173d6 (patch)
tree69850e82ea83b7f3327b59fcd9257e9dae643ef8
parentacdb3608cb1faf18826981ba2fecd8e7781e5e4b (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.
-rw-r--r--ide/ide_slave.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index d8fdfdb1b..6c7ca4f8e 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -508,7 +508,6 @@ let rec parse = function
let () = Coqtop.toploop_init := (fun coq_args extra_args ->
let args = parse extra_args in
- Flags.quiet := true;
CoqworkmgrApi.(init High);
coq_args, args)