diffblue-cbmc/scripts/run_lint.sh

#!/bin/bash

script_folder=`dirname $0`

$script_folder/run_diff.sh CPPLINT "$@"
Adding script to run lint check on modified lines Bash script that uses blame on a range of commits to work out what lines have been touched since master. Finally it uses grep to filter the output of the linting script based only on lines that have been modified. The yml file that runs the linter has been updated to run this script. 2017-01-06 22:58:23 +08:00			`#!/bin/bash`

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 2017-01-12 18:59:44 +08:00			script_folder=`dirname $0`
Adding script to run lint check on modified lines Bash script that uses blame on a range of commits to work out what lines have been touched since master. Finally it uses grep to filter the output of the linting script based only on lines that have been modified. The yml file that runs the linter has been updated to run this script. 2017-01-06 22:58:23 +08:00
Rename run_lint to run_diff 2017-07-03 18:13:18 +08:00			`$script_folder/run_diff.sh CPPLINT "$@"`