diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2019-04-10 18:16:10 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-04-10 18:16:10 +0200 |
| commit | 07b76c0376eef34fcbf52ecc21074c5084f980f5 (patch) | |
| tree | 9b947d26c956a370b3f7c18c0e49062cb9bc2094 /doc/tools | |
| parent | e33764744cb2bf72ee77c823c3beeb6dc870d2dc (diff) | |
| parent | 7a0dfc04aa85d0a7c5f317252e9eb917d0aef788 (diff) | |
Merge pull request #27170 from timoschwarzer/allow-whitespaces-in-warning-ignore-comments
Allow whitespaces in warning-ignore comments
Diffstat (limited to 'doc/tools')
0 files changed, 0 insertions, 0 deletions