blob: 9f24960fff824624a4ba2bc4a62a275881d1d576 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
#!/usr/bin/env bash
set -e
# This script depends (at least) on git and jq.
# It should be used like this: dev/tools/merge-pr.sh /PR number/
#TODO: check arguments and show usage if relevant
PR=$1
CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
git fetch "$REMOTE" "refs/pull/$PR/head"
API=https://api.github.com/repos/coq/coq
BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')
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
echo
if [[ ! $REPLY =~ ^[Yy]$ ]]
then
exit 1
fi
fi;
if [ "$STATUS" != "success" ]; then
echo "CI status is \"$STATUS\""
read -p "Bypass? [y/N] " -n 1 -r
echo
if [[ ! $REPLY =~ ^[Yy]$ ]]
then
exit 1
fi
fi;
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 --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then
echo "******************************************"
echo "** WARNING: does this PR have overlays? **"
echo "******************************************"
fi
|
