diff options
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/checkmans.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/checkmans.sh b/tools/checkmans.sh index 618f8ba88..9a137780c 100755 --- a/tools/checkmans.sh +++ b/tools/checkmans.sh @@ -70,7 +70,7 @@ remove_repeats() cd $(git rev-parse --show-toplevel) for I in $( - find -path './autom4te.cache' -prune -o -name '*[[:alpha:]].[1-8]' -print + find -path './autom4te.cache' -prune -o -path './.libs' -prune -o -name '*[[:alpha:]].[1-8]' -print ); do MAN_FILE=${I##*/} MAN_LIST[${MAN_FILE%%.[0-9]}]=1 |