diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 10:05:35 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 10:05:35 +0100 |
| commit | 5213bcdfd2baa5e2e652eaa63fff8d3268959489 (patch) | |
| tree | b2eee60485610d9bb0e8dff44f94ad85c693b0e5 /plugins/setoid_ring | |
| parent | db6d0bbf0a881b8867f3411acbedcba5c946c8f8 (diff) | |
| parent | 6ef5c101facffc902577519bcfb0ffdcbe1be166 (diff) | |
Merge PR #6789: Check whitespace errors per-commit.
Diffstat (limited to 'plugins/setoid_ring')
0 files changed, 0 insertions, 0 deletions