Mention the PR author in mergebot PRs (#8390)
Hopefully, this should help prevent mergebot PRs from being unnoticed by generating a GitHub notification to the author.
Test Plan: Use ghstack to push a PR (get something like gh/kirklandsign/17/head). In .github/scripts/propose_ghstack_orig_pr.py, remove print("The PR (and stack above) is not merged yet, skipping") and return after it. Then python .github/scripts/propose_ghstack_orig_pr.py --repo pytorch/executorch --ref refs/heads/gh/kirklandsign/17/head S
Scott Wolchok committed
3b3ff5ce2ae22c4cd9c385131767b5deb047a25b
Parent: 8c9a42c
Committed by GitHub <noreply@github.com>
on 2/12/2025, 11:04:46 PM