From a2e34cd42ef6a4327e701416114c6b8b85a173d6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 31 Mar 2018 18:47:52 +0200 Subject: [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. --- ide/ide_slave.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'ide') 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) -- cgit v1.2.3