-
|
I was wondering how to get assigned to a PR. It helps to see the ongoing PRs by user, etc. I looked into https://github.com/tlaplus/vscode-tlaplus/blob/master/CONTRIBUTING.md and didn't find any mention of that. Should I just tag the maintainers? If so, which ones? (I don't want to tag/spam people I shouldn't =) ) |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment 3 replies
-
|
I have no idea how this is done on Github. I can't speak for the other maintainers, but for now, feel free to tag or spam me directly. |
Beta Was this translation helpful? Give feedback.
-
|
This area:
|
Beta Was this translation helpful? Give feedback.
-
|
I’d like to request a review of #386 from @hwayne, but the GitHub UI doesn’t show this handle in the reviewer drop-down, and I’m unable to add the handle manually. |
Beta Was this translation helpful? Give feedback.
-
|
I can't request any reviews neither; thank you for the assignments btw^^ |
Beta Was this translation helpful? Give feedback.
I have no idea how this is done on Github. I can't speak for the other maintainers, but for now, feel free to tag or spam me directly.