Wait for GitHub to process git push before updating PR
Updating the pull request (with gh pr edit) right after a git push
was causing the synchronize webhook to be fired twice. This results
in GitHub Actions being started twice as well.
This commit adds a check before editing a pull request that compares
the current HEAD commit with the head id on GitHub. If these don't
match, it means that GitHub has not yet processed the git push.
We check this up to five times, waiting one second between checks.
Wait for GitHub to process
git pushbefore updating PRUpdating the pull request (with
gh pr edit) right after a git push was causing thesynchronizewebhook to be fired twice. This results in GitHub Actions being started twice as well.This commit adds a check before editing a pull request that compares the current HEAD commit with the head id on GitHub. If these don't match, it means that GitHub has not yet processed the git push. We check this up to five times, waiting one second between checks.
Fixes #189