aboutsummaryrefslogtreecommitdiff
path: root/dev/tools/check-owners.sh
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-04-05 11:03:58 +0200
committerGaëtan Gilbert2018-04-26 13:13:33 +0200
commitaed2eec838151dfe13e9ad2697b7ccfe319778df (patch)
treecc0ee7bd8c0d58f2478bda32cbde332e4009384d /dev/tools/check-owners.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.sh')
-rwxr-xr-xdev/tools/check-owners.sh6
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/tools/check-owners.sh b/dev/tools/check-owners.sh
index c28ab5cb63..1a97508abb 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}