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 e54ebed37..4b149d077 100755 --- a/tools/checkmans.sh +++ b/tools/checkmans.sh @@ -39,7 +39,7 @@ trap "rm -f ${ERROR_FILE}" 0 for I in $( find $(git rev-parse --show-toplevel) -name '*.[1-8]' | - egrep -v '(Documentation|.git|/.libs/|autom4te.cache|ru/ddate)' + egrep -v '(Documentation|.git|/.libs/|autom4te.cache)' ); do # FIXME: the determination whether a manual does include # should probably be somewhat smarter. |