diff options
| author | Maxime Dénès | 2017-11-23 10:17:33 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-23 16:12:44 +0100 |
| commit | 99599ecf3a92e458e96722601eefa56dd17ad774 (patch) | |
| tree | e0143ec77b2ba8143a198acea4c69c1da0d5ad0c /API/API.mli | |
| parent | eb91ccaf236bc9a60a1e216b76a0a42980c072a7 (diff) | |
Add PR filter used by RM to the contributing guide.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions