aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools/check-owners-pr.sh
blob: d2910279b52814f43ebd9f2231f877c90c444058 (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
#!/usr/bin/env sh

usage() {
    { echo "usage: $0 PR [ARGS]..."
      echo "A wrapper around check-owners.sh to check owners for a PR."
      echo "Assumes upstream is the canonical Coq repository."
      echo "Assumes the PR is against master."
      echo
      echo "  PR: PR number"
      echo "  ARGS: passed through to check-owners.sh"
    } >&2
}

case "$1" in
    "--help"|"-h")
        usage
        if [ $# = 1 ]; then exit 0; else exit 1; fi;;
    "")
        usage
        exit 1;;
esac

PR="$1"
shift

# this puts both refs in the FETCH_HEAD file but git rev-parse will use the first
git fetch upstream "+refs/pull/$PR/head" master

head=$(git rev-parse FETCH_HEAD)
base=$(git merge-base upstream/master "$head")

git diff --name-only -z "$base" "$head" | xargs -0 dev/tools/check-owners.sh "$@"