From 4bcf7131c149db2cbd2e95f392a04e485cbfeb58 Mon Sep 17 00:00:00 2001 From: Anders Kaseorg Date: Wed, 3 Feb 2021 12:07:06 -0800 Subject: [PATCH] push-to-pull-request: Wait for GitHub background update before merge. Signed-off-by: Anders Kaseorg --- tools/push-to-pull-request | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/tools/push-to-pull-request b/tools/push-to-pull-request index 27d13cb5cc..8fabc819af 100755 --- a/tools/push-to-pull-request +++ b/tools/push-to-pull-request @@ -142,5 +142,17 @@ if [ -n "$tracking_ref" ]; then fi if [ "$merge" ]; then + tries=10 + sha="$(git rev-parse @)" + while + out=$(git ls-remote -- "$remote" "refs/pull/$pr_id/head") + [ "$out" != "$sha refs/pull/$pr_id/head" ] + do + if ! ((--tries)); then + echo 'error: Push was not observed in PR' >&2 + exit 1 + fi + sleep 1 + done git push -- "$remote" "@:$pr_base_ref" fi