Stream: Coq Platform devs & users

Topic: GitHub issue management


view this post on Zulip Karl Palmskog (Sep 30 2020 at 15:01):

as a start, maybe we can at least introduce some labels for issues in the repo? Now it seems like a haphazard conglomeration of different problems

view this post on Zulip Théo Zimmermann (Sep 30 2020 at 15:14):

Any suggestion for the labels? It looks like one of them needs to be "package inclusion", one might be "policy discussion". What about the others?

view this post on Zulip Karl Palmskog (Sep 30 2020 at 15:16):

view this post on Zulip Karl Palmskog (Sep 30 2020 at 15:20):

also:

view this post on Zulip Théo Zimmermann (Sep 30 2020 at 15:29):

What about https://github.com/coq/platform/issues/2?

view this post on Zulip Karl Palmskog (Sep 30 2020 at 15:30):

hmm, maybe policy or advertising or outreach

view this post on Zulip Karl Palmskog (Sep 30 2020 at 15:35):

also, I believe these can now be closed since the packages are part of the beta release:


Last updated: Jan 30 2023 at 11:03 UTC