diff options
| author | Maxime Dénès | 2018-09-10 15:07:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-10 15:07:42 +0200 |
| commit | 90a0357108769355025e8f15a6fbf6766aed8d44 (patch) | |
| tree | e72decfdd385c649334d422f5b5ec6cf6b02220f /dev/include | |
| parent | 2413031f6a5eeb0b49545a0b8ae312a99cbb5659 (diff) | |
| parent | a325b3026c2569f3c60364509d9b08925c16c6dc (diff) | |
Merge PR #8323: Owners of Makefile.{ci,doc} are teams {ci,doc}-maintainers.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions