Relax port lint rule for patchfile naming

[Ryan Schmidt]

I think we should relax the restrictions on patchfile naming currently implemented in port lint. I'd like to discuss it here before I file a ticket.

Currently, we complain if a patchfile is not named "patch-*.diff". But we already have many files in the repository named "*.patch" for example. We are proposing adding a job to the buildbot that automatically runs port lint, and we don't want it to complain about a requirement we're not following in practice anyway.

The only reason why I originally wanted a lint check was that we used to have patchfile names like "patch-*", with no separate extension. This resulted in patchfile names like "patch-foo.c", which, when opened into an editor that configures syntax highlighting based on filename extension, would be syntax highlighted as if they were a .c file, when it was desired to see syntax highlighting that was tailored for a diff.

I would be happy if lint were changed to just check that patchfile names end with .diff or .patch. Would anyone object to that?