diff options
| author | Maxime Dénès | 2017-10-06 12:47:22 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-06 12:47:22 +0200 |
| commit | f1598b00219a951e94036cb7f48a8fe1309025f1 (patch) | |
| tree | 62dd9a6da381137e61a6b732ae0ba806d822c5cc /API/API.mli | |
| parent | 6cb1829829de5edfe733b901c38a8b39ba03ef56 (diff) | |
| parent | 248fffe64ee42137822ba438dfb378defbe1aa05 (diff) | |
Merge PR #1127: Shorten the .gitattributes file.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions