diff options
| author | Gaëtan Gilbert | 2018-05-07 16:51:58 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-07 16:51:58 +0200 |
| commit | 273292326de103c64cc7c5c3708c484c7064f551 (patch) | |
| tree | f2b139a6ab9b64e67b87651f633ec0a134a0958d /kernel/type_errors.ml | |
| parent | aed2eec838151dfe13e9ad2697b7ccfe319778df (diff) | |
Add CODEOWNERS entry for check-owners*.sh
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions