Browse Source

Merge pull request #4731

c53b1ec Fix github-merge with git version 2.1.0 (Gavin Andresen)
0.10
Wladimir J. van der Laan 10 years ago
parent
commit
2fb886bffb
No known key found for this signature in database
GPG Key ID: 74810B012346C9A6
  1. 4
      contrib/devtools/github-merge.sh

4
contrib/devtools/github-merge.sh

@ -49,11 +49,11 @@ fi
# Initialize source branches. # Initialize source branches.
git checkout -q "$BRANCH" git checkout -q "$BRANCH"
if git fetch -q "$HOST":"$REPO" "+refs/pull/$PULL/*:refs/heads/pull/$PULL/*"; then if git fetch -q "$HOST":"$REPO" "+refs/pull/$PULL/*:refs/heads/pull/$PULL/*"; then
if ! git log -1q "refs/heads/pull/$PULL/head" >/dev/null 2>&1; then if ! git log -q -1 "refs/heads/pull/$PULL/head" >/dev/null 2>&1; then
echo "ERROR: Cannot find head of pull request #$PULL on $HOST:$REPO." >&2 echo "ERROR: Cannot find head of pull request #$PULL on $HOST:$REPO." >&2
exit 3 exit 3
fi fi
if ! git log -1q "refs/heads/pull/$PULL/merge" >/dev/null 2>&1; then if ! git log -q -1 "refs/heads/pull/$PULL/merge" >/dev/null 2>&1; then
echo "ERROR: Cannot find merge of pull request #$PULL on $HOST:$REPO." >&2 echo "ERROR: Cannot find merge of pull request #$PULL on $HOST:$REPO." >&2
exit 3 exit 3
fi fi

Loading…
Cancel
Save