diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-04 16:28:36 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-04 16:28:36 +0200 |
commit | ea1d8bbc3cddbd661439155240bd6f9ec477d84c (patch) | |
tree | b5c5d983d1d373042ce61f0fd277c309043a458a /.github | |
parent | 11fe480932306e3bd702b19674f385f5e36398b7 (diff) |
check-owners.sh: add --show-patterns and --owner options
```bash
$ dev/tools/check-owners.sh --show-patterns Makefile Makefile.build
/Makefile*: @letouzey
$ dev/tools/check-owners.sh --owner '@gares' stm/stm.ml interp/declare.ml
stm/stm.ml: @gares
$ dev/tools/check-owners.sh --show-patterns --owner '@gares' stm/*.ml interp/*.ml
/stm/: @gares
```
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions