aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools/check-owners-pr.sh
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-05 11:03:58 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-26 13:13:33 +0200
commitaed2eec838151dfe13e9ad2697b7ccfe319778df (patch)
treecc0ee7bd8c0d58f2478bda32cbde332e4009384d /dev/tools/check-owners-pr.sh
parentea1d8bbc3cddbd661439155240bd6f9ec477d84c (diff)
Add check-owners-pr.sh wrapper around check-owners
``` $ dev/tools/check-owners-pr.sh 6809 --show-patterns --owner '@MSoegtropIMC' remote: Counting objects: 93, done. remote: Compressing objects: 100% (3/3), done. remote: Total 93 (delta 47), reused 50 (delta 47), pack-reused 43 Unpacking objects: 100% (93/93), done. From github.com:coq/coq * branch refs/pull/6809/head -> FETCH_HEAD * branch master -> FETCH_HEAD /dev/build/windows: @MSoegtropIMC ```
Diffstat (limited to 'dev/tools/check-owners-pr.sh')
-rwxr-xr-xdev/tools/check-owners-pr.sh32
1 files changed, 32 insertions, 0 deletions
diff --git a/dev/tools/check-owners-pr.sh b/dev/tools/check-owners-pr.sh
new file mode 100755
index 000000000..d2910279b
--- /dev/null
+++ b/dev/tools/check-owners-pr.sh
@@ -0,0 +1,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 "$@"