frozenleaves/pytorch
1
0
Fork 0
mirror of https://github.com/pytorch/pytorch.git synced 2025-10-21 05:34:18 +08:00
Code Issues Packages Projects Releases Wiki Activity

Fix merging label removal (#100433)

Browse Source 
During regular merge process, when `GitHubPR` object is created, it does not have `merging` label and when label is added it does not update existing `GitHubPR` object either

To fix the problem, call REST API wrapper `gh_remove_label` directly. Worst case that can happen, if label is already removed at this point, is that it will be printed to the stderr, which is not rendered on HUD anyway

Pull Request resolved: https://github.com/pytorch/pytorch/pull/100433
Approved by: https://github.com/PaliC, https://github.com/kit1980
This commit is contained in:
Nikita Shulga
2023-05-02 00:30:09 +00:00
committed by PyTorch MergeBot
parent f143c92739
commit 5daef13883
2 changed files with 7 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
.github/scripts/trymerge.py vendored
View File

@ -1049,10 +1049,6 @@ class GitHubPR:
full_label = f"{label_base}X{count}"
gh_add_labels(self.org, self.project, self.pr_num, [full_label])
def remove_label(self, label: str) -> None:
if self.get_labels() is not None and label in self.get_labels():
gh_remove_label(self.org, self.project, self.pr_num, label)
def merge_into(
self,
repo: GitRepo,
@ -2049,7 +2045,7 @@ def main() -> None:
else:
print("Missing comment ID or PR number, couldn't upload to Rockset")
finally:
pr.remove_label(MERGE_IN_PROGRESS_LABEL)
gh_remove_label(org, project, args.pr_num, MERGE_IN_PROGRESS_LABEL)
if __name__ == "__main__":