Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
build: add a retry on
git push
in merge-pr.sh
Github sometimes takes a few seconds to figure out that after a force-push to a branch, we are still allowed to merge it to main. So this does a sleep/retry, once, in the event that the first push fails.
- Loading branch information