diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-11 15:57:19 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-11 15:57:19 +0100 |
| commit | 0275b5802ffd416dd0ed739955445a1c3c0287e9 (patch) | |
| tree | 96ef08333268e3d99dc3d04855e1d4a5729af43f /configure.ml | |
| parent | 4cd5ba6019ecf8a9c41c8594a5446286af725793 (diff) | |
| parent | f1168b816dcbd8ee45787da1251ba5b2a68176d5 (diff) | |
Merge PR #6331: Linter: skip PRs older than the linter.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions