diff options
| author | Gaëtan Gilbert | 2018-04-04 16:28:36 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 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