Skip to content

Commit 81941be

Browse files
Merge pull request #428 from thk123/bug/deleted-file-lint
Run lint script handling deleted files
2 parents 094c76d + a4954cd commit 81941be

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

scripts/run_lint.sh

+6
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,12 @@ IFS=$'\n'
4646
are_errors=0
4747

4848
for file in $diff_files; do
49+
# If the file has been deleted we don't want to run the linter on it
50+
if ! [[ -e $file ]]
51+
then
52+
continue
53+
fi
54+
4955
# We build another grep filter the output of the linting script
5056
lint_grep_filter="^("
5157

0 commit comments

Comments
 (0)