Zulip Chat Archive
Stream: sphere eversion
Topic: github project
Yury G. Kudryashov (Jul 24 2022 at 14:31):
Is it OK with you if I create a github project for "sphere eversion" and use it as a tag for PRs related to the project?
Patrick Massot (Jul 24 2022 at 15:36):
It is ok but I don't understand what you expect to gain.
Yury G. Kudryashov (Jul 24 2022 at 15:37):
We can use it as another label that does not pollute the list of labels. E.g., you can search for these PRs and review them.
Yury G. Kudryashov (Jul 24 2022 at 19:20):
https://github.com/leanprover-community/mathlib/projects/17#card-84464438
Last updated: Dec 20 2023 at 11:08 UTC