diff options
Diffstat (limited to 'build-aux')
| -rwxr-xr-x | build-aux/lint-generic | 5 | ||||
| -rwxr-xr-x | build-aux/lint-unknown | 5 |
2 files changed, 0 insertions, 10 deletions
diff --git a/build-aux/lint-generic b/build-aux/lint-generic index 70e814a..d982527 100755 --- a/build-aux/lint-generic +++ b/build-aux/lint-generic @@ -14,11 +14,6 @@ err() { r=0 for filename in "$@"; do - if ! { [ -f "$filename" ] && ! [ -h "$filename" ]; }; then - # Ignore non-files - continue - fi - # File header ########################################################## shebang="$(sed -n '1{/^#!/{/^#!\/hint\//q; p;};}' "$filename")" diff --git a/build-aux/lint-unknown b/build-aux/lint-unknown index dda9541..bc23a81 100755 --- a/build-aux/lint-unknown +++ b/build-aux/lint-unknown @@ -14,11 +14,6 @@ err() { r=0 for filename in "$@"; do - if ! { [ -f "$filename" ] && ! [ -h "$filename" ]; }; then - # Ignore non-files - continue - fi - err "$filename" 'cannot lint unknown file type' done exit $r |