Stream: Coq devs & plugin devs

Topic: Should coqc send Print to stdout?

view this post on Zulip Ali Caglayan (Aug 17 2020 at 23:58):

Hi, why does coqc send Print (and Check and Time) to stdout? Can this be disabled?

view this post on Zulip Jason Gross (Aug 19 2020 at 19:55):

Why not just comment out the directives if you don't want them to print? (AFAIK, there's not currently a way to disable it, though you can Redirect to a file. You can request a flag to disable the behavior, though. (I don't think it should be turned off unconditionally, though, as I depend on this in some of my projects.))

Last updated: Dec 05 2023 at 12:01 UTC