diff options
| author | Gaëtan Gilbert | 2019-06-05 09:58:07 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-06 17:59:07 +0200 |
| commit | 8d2b88c80ec77090928a9da3d6b00e25a5ed6fb1 (patch) | |
| tree | a9704c7b12081688b8dce597a33fae2b67fb7ec6 /dev/doc/changes.md | |
| parent | 90c1084ba489415f8df588c43e088491bc6be450 (diff) | |
CI: Test ml compilation of each commit in a PR in lint job
Diffstat (limited to 'dev/doc/changes.md')
0 files changed, 0 insertions, 0 deletions