Stream: Coq devs & plugin devs

Topic: kind: wish


view this post on Zulip Gaëtan Gilbert (Oct 15 2021 at 11:14):

what's this label for?

view this post on Zulip Ana de Almeida Borges (Oct 15 2021 at 11:16):

Something like feature request?

view this post on Zulip Gaëtan Gilbert (Oct 15 2021 at 11:56):

but there's already kind:feature

view this post on Zulip Pierre Roux (Oct 15 2021 at 11:59):

Isn't feature rather used for new features introduction (PR) while wish is for issues?

view this post on Zulip Gaëtan Gilbert (Oct 15 2021 at 11:59):

no

view this post on Zulip Guillaume Melquiond (Oct 15 2021 at 12:01):

I would have the same interpretation as Pierre. But that does not explain why we have two separate labels rather than a single label kind:wish/feature.

view this post on Zulip Théo Zimmermann (Oct 15 2021 at 12:54):

When migrating from Bugzilla, I initially hoped that we would use the same labels in issues and PRs but it hasn't really been a success in practice, and I guess that why we have the duality kind: bug / kind: fix and kind: wish / kind: enhancement / kind: feature nowadays.


Last updated: Oct 13 2024 at 01:02 UTC