Zulip Chat Archive
Stream: mathlib4
Topic: file not in the list
Jakob von Raumer (Dec 06 2022 at 09:39):
Wanted to file a PR for combinatorics.quiver.push, but it's not in the wiki list?
Jakob von Raumer (Dec 06 2022 at 09:40):
Should I just add it?
Scott Morrison (Dec 06 2022 at 09:59):
Yes, it should be fine to just add it. We need to automate this still...
Jakob von Raumer (Dec 06 2022 at 10:01):
I guess as long as Johan's status page shows them it's not that bad
Last updated: Dec 20 2023 at 11:08 UTC