diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-11-28 15:05:52 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-11-29 15:46:17 +0100 |
| commit | bc1fb4be47578b4da554aef69150acd77e82aba1 (patch) | |
| tree | b404488198794cf3c445236554865b61e780a2ae /dev/tools | |
| parent | b23df225c7df7883af6ecfa921986cfb6fd3cd7c (diff) | |
Fix PR merge script.
Was still relying on the existence of user-configured /pr/.
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/merge-pr.sh | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index f770004a5..63c42629c 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -15,12 +15,12 @@ API=https://api.github.com/repos/coq/coq BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'` -COMMIT=`git rev-parse $REMOTE/pr/$PR` +COMMIT=`git rev-parse FETCH_HEAD` STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'` if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then echo "Wrong base branch" - read -p "Bypass? [y/n] " -n 1 -r + read -p "Bypass? [y/N] " -n 1 -r echo if [[ ! $REPLY =~ ^[Yy]$ ]] then @@ -30,7 +30,7 @@ fi; if [ $STATUS != "success" ]; then echo "CI status is \"$STATUS\"" - read -p "Bypass? [y/n] " -n 1 -r + read -p "Bypass? [y/N] " -n 1 -r echo if [[ ! $REPLY =~ ^[Yy]$ ]] then @@ -38,7 +38,7 @@ if [ $STATUS != "success" ]; then fi fi; -git merge -S --no-ff $REMOTE/pr/$PR -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e +git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e # TODO: improve this check if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then |