The only thing it did over ‘tools/lint --skip=gitlint’ was redundantly run mypy again. Signed-off-by: Anders Kaseorg <anders@zulip.com>