diff options
Diffstat (limited to 'dist/checkman.awk')
| -rw-r--r-- | dist/checkman.awk | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dist/checkman.awk b/dist/checkman.awk index 947888dc..eebb4370 100644 --- a/dist/checkman.awk +++ b/dist/checkman.awk @@ -446,7 +446,7 @@ END { gsub("\\(", " \\(", b) gsub("\\)", "\\)", b) split(tolower(i), a, "/") - print "egrep -in '^\\.IR.*" b "' $PLAN9/man/man*/* # Need " tolower(i) |"sort" + print "grep -in '^\\.IR.*" b "' $PLAN9/man/man*/* # Need " tolower(i) |"sort" } } close("sort") |