diff options
| author | Maxime Dénès | 2017-11-06 11:25:13 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-06 11:25:13 +0100 |
| commit | ca5e66889022f7ba7d3b6003aaccad3ec521e878 (patch) | |
| tree | 34feb95956815d4edb4896c56d8f81355e17dfdf /API/API.mli | |
| parent | dc6f4b07c38b416b1771bf7436af9303f25f0c1e (diff) | |
| parent | 82db238369a6f5b3de1fa629c6852ffe8d447b3f (diff) | |
Merge PR #6085: Update .mailmap with a jkloos alias
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions