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 /ide | |
| 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')
| -rw-r--r-- | ide/ide_slave.ml | 1 |
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) |