diff options
| author | Théo Zimmermann | 2019-02-20 16:36:56 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-28 15:44:29 +0100 |
| commit | b46b8cbe886ea1e06377843134e9c588394acc5f (patch) | |
| tree | ff59757e0ebf35fc0451777e607c5592aab8cb12 /dev/base_include | |
| parent | 27838d59f12fde650191c61f3d2168daa1ac2bd3 (diff) | |
Fix #9110: mention check-owners-pr.sh
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions