Stream: Coq devs & plugin devs

Topic: ✔ "kind: feature request" tag


view this post on Zulip Ali Caglayan (Nov 10 2021 at 13:02):

I've created this tag since I seem to recall people getting confused about "kind: wish".

view this post on Zulip Gaëtan Gilbert (Nov 10 2021 at 13:04):

kind:feature was plenty though

view this post on Zulip Ali Caglayan (Nov 10 2021 at 13:05):

But that's to do with PRs no?

view this post on Zulip Gaëtan Gilbert (Nov 10 2021 at 13:06):

no

view this post on Zulip Ali Caglayan (Nov 10 2021 at 13:06):

I'll get rid of it then and update the description of "kind: feature"

view this post on Zulip Notification Bot (Nov 10 2021 at 13:08):

Ali Caglayan has marked this topic as resolved.


Last updated: Oct 13 2024 at 01:02 UTC