From fe47dec1ea4fe863abe07e68fab1823a289a647a Mon Sep 17 00:00:00 2001 From: NathanJPhillips Date: Thu, 12 Jan 2017 10:59:44 +0000 Subject: [PATCH] Allow lint to be called from any folder This allows use of the lint script without changing to the root of the CBMC folder first; e.g. to lint a non-CBMC project --- scripts/run_lint.sh | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/scripts/run_lint.sh b/scripts/run_lint.sh index f2f1a41d811..23f6d33b1fb 100755 --- a/scripts/run_lint.sh +++ b/scripts/run_lint.sh @@ -2,6 +2,8 @@ set -e +script_folder=`dirname $0` + if [[ "$#" -ne 2 ]] then echo "Script for running the CPP linter only on modified lines." @@ -12,10 +14,10 @@ then exit 1 fi -if ! [[ -e scripts/cpplint.py ]] +if ! [[ -e $script_folder/cpplint.py ]] then - echo "Lint script could not be found in the scripts directory" - echo "Ensure cpplint.py is inside the scripts directory then run again" + echo "Lint script could not be found in the $script_folder directory" + echo "Ensure cpplint.py is inside the $script_folder directory then run again" exit 1 fi @@ -81,7 +83,7 @@ for file in $diff_files; do # Run the linting script and filter by the filter we've build # of all the modified lines # The errors from the linter go to STDERR so must be redirected to STDOUT - result=`python scripts/cpplint.py $file 2>&1 | { grep -E "$lint_grep_filter" || true; }` + result=`python $script_folder/cpplint.py $file 2>&1 | { grep -E "$lint_grep_filter" || true; }` # Providing some errors were relevant we print them out if [ "$result" ]