Merge pull request #4116 from leoetlino/lint-real-fix Tools: Fix the lint script (for real, this time -- and the last time)
