diff options
Diffstat (limited to 'tools/lint.sh')
-rwxr-xr-x | tools/lint.sh | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/tools/lint.sh b/tools/lint.sh deleted file mode 100755 index 5264112..0000000 --- a/tools/lint.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/bin/sh - - -if ! command -v splint 2> /dev/null -then - echo "Please install splint (http://splint.org/)!" - exit 1 -fi - -find . -type f -iname '*.c' | xargs splint |