diff options
| author | Gaëtan Gilbert | 2018-12-14 15:19:19 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-21 15:33:36 +0100 |
| commit | b80e0b73e4417f414d723cfb2f424ecec321767d (patch) | |
| tree | 6530c90fe39592bac554bfdb588bee60ebd43de2 /kernel/nativecode.ml | |
| parent | ee98d818791d8f92674934cda02bfcb3667013c9 (diff) | |
Move lint job to gitlab
This changes the semantics a bit since we don't have
TRAVIS_COMMIT_RANGE anymore, instead we do per-commit linting for the
commits since the last merge commit.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions