diff options
| author | Gaëtan Gilbert | 2019-02-18 13:28:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 13:29:35 +0100 |
| commit | 136b61ae70113922330de032f005b4acb50bc800 (patch) | |
| tree | 111924aea1a33edd65975b09bef1abdddc6eeca8 /plugins | |
| parent | f8d6c322783577b31cf55f8b55568ac56104202b (diff) | |
Fix per-commit linting with bot merges
When the bot auto-merged the linter saw no commits to lint, eg
https://gitlab.com/coq/coq/-/jobs/162893603
I'm pushing from a non-current master so we will see if this works.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions