Stream: Coq devs & plugin devs

Topic: Close as not planned.

view this post on Zulip Théo Zimmermann (May 27 2022 at 16:56):

GitHub now has a feature to distinguish closed issues because they were completed (purple) and closed issues because they were not planned (gray). I just changed the status of https://github.com/coq/coq/issues/14719 to test this. We could change the status of all past won't fix issues but I'm afraid this would trigger notifications for everyone.

view this post on Zulip Wolf Honore (May 27 2022 at 17:55):

It did trigger a notification for me as the author of the issue. Probably it does for everyone who's subscribed to it?

view this post on Zulip Théo Zimmermann (May 28 2022 at 10:23):

That's my guess.

Last updated: Jun 05 2023 at 10:01 UTC