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 /.github | |
| 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
```
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions