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 "$@"
|
