Skip to content

Commit 36dee83

Browse files
Check that filter_lint_by_diff.py exists
1 parent 6bba4ab commit 36dee83

File tree

1 file changed

+7
-0
lines changed

1 file changed

+7
-0
lines changed

scripts/run_lint.sh

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,13 @@ then
2020
exit 1
2121
fi
2222

23+
if ! [[ -e $script_folder/filter_lint_by_diff.py ]]
24+
then
25+
echo "Lint filter script could not be found in the $script_folder directory"
26+
echo "Ensure filter_lint_by_diff.py is inside the $script_folder directory then run again"
27+
exit 1
28+
fi
29+
2330
if [[ "$#" -gt 0 ]]
2431
then
2532
git_start=$1

0 commit comments

Comments
 (0)