diff options
Diffstat (limited to 'contrib')
-rwxr-xr-x | contrib/scripts/check-texinfo.awk.in | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/contrib/scripts/check-texinfo.awk.in b/contrib/scripts/check-texinfo.awk.in index 37e2c9f20..3d6a1c643 100755 --- a/contrib/scripts/check-texinfo.awk.in +++ b/contrib/scripts/check-texinfo.awk.in | |||
@@ -5,7 +5,7 @@ | |||
5 | # | 5 | # |
6 | # exception to add: ignore license files. | 6 | # exception to add: ignore license files. |
7 | # exception to add: uref's can go above 79 chars. | 7 | # exception to add: uref's can go above 79 chars. |
8 | 8 | # write functions to avoid more text if possible. | |
9 | 9 | ||
10 | BEGIN { | 10 | BEGIN { |
11 | printf "Running basic texinfo linters\n" ; | 11 | printf "Running basic texinfo linters\n" ; |
@@ -56,4 +56,9 @@ BEGIN { | |||
56 | printf "...lines containing a popular typo\n" ; | 56 | printf "...lines containing a popular typo\n" ; |
57 | print FILENAME":"NR":"$0 ; | 57 | print FILENAME":"NR":"$0 ; |
58 | } | 58 | } |
59 | |||
60 | if (/the the/) { | ||
61 | printf "...lines containing a popular typo\n" ; | ||
62 | print FILENAME":"NR":"$0 ; | ||
63 | } | ||
59 | } | 64 | } |