You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: templates/contribute/index.md
+5-2Lines changed: 5 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -162,12 +162,15 @@ Labels can only be edited directly by "GitHub collaborators", which is approxima
162
162
However, anyone can add/remove the labels below by writing the following commands in a comment on the PR (each on its own line):
163
163
-`awaiting-author` will add the **"awaiting-author"** label
164
164
-`-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.
165
167
-`WIP` will add the **"WIP"** label
166
168
-`-WIP` will remove the **"WIP"** label
167
169
-`easy` will add the **"easy"** label
168
170
-`-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-).
171
174
172
175
This list is exhaustive. If you would like to add a different label, please, bring it up on Zulip!
0 commit comments