Skip to content

Commit 478f0f4

Browse files
authored
chore: update labels which can be added through comments (#780)
this documents the changes in the following PR: - [ ] depends on: leanprover-community/mathlib4#34683
1 parent 47baa4c commit 478f0f4

File tree

1 file changed

+5
-2
lines changed

1 file changed

+5
-2
lines changed

templates/contribute/index.md

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -162,12 +162,15 @@ Labels can only be edited directly by "GitHub collaborators", which is approxima
162162
However, anyone can add/remove the labels below by writing the following commands in a comment on the PR (each on its own line):
163163
- `awaiting-author` will add the **"awaiting-author"** label
164164
- `-awaiting-author` will remove the **"awaiting-author"** label
165+
- `awaiting-zulip` will add the **"awaiting-zulip"** label
166+
- `-awaiting-zulip` will remove the **"awaiting-zulip"** label. Use this once a decision has been reached and has been implemented.
165167
- `WIP` will add the **"WIP"** label
166168
- `-WIP` will remove the **"WIP"** label
167169
- `easy` will add the **"easy"** label
168170
- `-easy` will remove the **"easy"** label
169-
- Similarly, the labels for use by contributors upstreaming work from the downstream projects **brownian**, **carleson**, **CFT**, **FLT**, **sphere-packing** and **toric** can also be added and removed in the same way.
170-
- Any topic label of the form `t-*` (e.g. `t-topology`) can also be added and removed in the same way. PRs are auto-labeled based on their contents, but sometimes the auto-labeling is incorrect or incomplete so this lets you manually override it. See [available topic labels](https://github.com/leanprover-community/mathlib4/labels?q=t-).
171+
- `help-wanted`, `-help-wanted`, `please-adopt`, `-please-adopt` can be used to mark a PR in need of external input.
172+
- Similarly, the labels for use by contributors upstreaming work from the downstream projects **brownian**, **carleson**, **CFT**, **FLT**, **infinity-cosmos**, **sphere-packing** and **toric** can also be added and removed in the same way.
173+
- Any topic label of the form `t-*` (e.g. `t-topology`), as well as the labels `CI` and `IMO`, can also be added and removed in the same way. PRs are auto-labeled based on their contents, but sometimes the auto-labeling is incorrect or incomplete so this lets you manually override it. See [available topic labels](https://github.com/leanprover-community/mathlib4/labels?q=t-).
171174

172175
This list is exhaustive. If you would like to add a different label, please, bring it up on Zulip!
173176

0 commit comments

Comments
 (0)