-
Paul Eggert authored
Do not match file names that end in '/', as they cannot be 'grep' hits nowadays. This prevents confusion when 'grep -r' reports a match in a file whose basename is ':12345:'. Conversely, do not require exactly the same sequence of spaces and tabs after both colons, and allow spaces or tabs before the second colon, as per the POSIX spec for 'grep' output.
56c6a28d