lint: Remove custom --no-gitlint option.
zulint already has --skip for this. Signed-off-by: Anders Kaseorg <anders@zulip.com>
This commit is contained in:
parent
c4a78d0832
commit
2e3c65a044
2 changed files with 3 additions and 6 deletions
|
@ -2,5 +2,5 @@
|
|||
|
||||
set -ev
|
||||
|
||||
tools/lint --no-gitlint
|
||||
tools/lint --skip=gitlint
|
||||
tools/run-mypy
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue