Errors erase printed output

[Lysxia]

Some commands and options cause output to be printed to the *response* window (e.g., Set Typeclasses Debug and plugins). However, when an error occurs, the window is cleared, even though it may contain essential information to understand the error.

Is there any way to see that output?

One work around is to run coqc on the command line, but if you use many options in _CoqProject it's a bit of a pain to pass them to coqc manually, when PG is otherwise a perfectly fine environment to stay in.

[cpitclaudel]

Is there any way to see that output?

Yes, you can inspect all output in the *coq* buffer. But there's a lot of stuff in there (you may want to temporarily turn off company-coq in those cases, if you use it, since it can generate noise in *coq*)

[Lysxia]

Oh I see! Thanks @cpitclaudel !

[cpitclaudel]

I'm not sure that this should be closed — it's not ideal to have to go to *coq*. I was just providing a workaround ^^

[Lysxia]

Fair enough!