diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-05 11:03:58 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 13:13:33 +0200 |
commit | aed2eec838151dfe13e9ad2697b7ccfe319778df (patch) | |
tree | cc0ee7bd8c0d58f2478bda32cbde332e4009384d | |
parent | ea1d8bbc3cddbd661439155240bd6f9ec477d84c (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
```
-rwxr-xr-x | dev/tools/check-owners-pr.sh | 32 | ||||
-rwxr-xr-x | dev/tools/check-owners.sh | 6 |
2 files changed, 35 insertions, 3 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 "$@" diff --git a/dev/tools/check-owners.sh b/dev/tools/check-owners.sh index c28ab5cb6..1a97508ab 100755 --- a/dev/tools/check-owners.sh +++ b/dev/tools/check-owners.sh @@ -73,7 +73,7 @@ done # so we create a valid .gitignore by removing all but the first field while read -r pat _; do - printf "%s\n" "$pat" >> .gitignore + printf '%s\n' "$pat" >> .gitignore done < .github/CODEOWNERS # associative array [file => owner] @@ -123,10 +123,10 @@ for f in "${files[@]}"; do done for f in "${!owners[@]}"; do - printf "%s: %s\n" "$f" "${owners[$f]}" + printf '%s: %s\n' "$f" "${owners[$f]}" done | sort -k 2 -k 1 # group by owner -# restort gitignore files +# restore gitignore files rm .gitignore find . -name .gitignore.bak -print0 | while IFS= read -r -d '' f; do base=${f%.bak} |