summaryrefslogtreecommitdiff
path: root/tools/lint.sh
diff options
context:
space:
mode:
Diffstat (limited to 'tools/lint.sh')
-rwxr-xr-xtools/lint.sh10
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