PR #1575 fix(scripts): sanity_check -> lint [ci skip]

fix(scripts): sanity_check -> lint [ci skip] #1575

mergify merged 3 commits into master from scripts_fix

fix(scripts): sanity_check -> lint [ci skip]

f6d48386

also fix in .gitignore

c1451f65

kim-em approved these changes on 2019-10-21

jcommelin added ready-to-merge

Merge branch 'master' into scripts_fix

9c276978

mergify merged 0b660a9f into master 6 years ago

mergify deleted the scripts_fix branch 6 years ago

Reviewers

kim-em

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone