Stream: VsCoq devs & users

Topic: Why does `Search` output to Notices?


view this post on Zulip Ali Caglayan (Apr 28 2021 at 12:38):

Why does Search output to Notices? Check and About output to the Ouput tab so it seems kind of arbitrary for search to put them here. Also it means that multiple searches get appended, and it gets difficult to understand the results.

view this post on Zulip Matthieu Sozeau (Apr 28 2021 at 15:32):

Agreed


Last updated: Jan 30 2023 at 18:04 UTC