check-diff shows at most 10 warnings

[bgilbert]

GitHub renders at most 10 annotations in the PR diff view and the workflow run summary page. An unlimited number of warnings is shown in the check-diff job log, but the log is less ergonomic, so usually it's not used when a reviewer is examining the diff. Thus it's possible that a reviewer might miss some changes.

Clearly indicate that some warnings have been elided, perhaps by emitting at most 9 warnings plus a notice to check the log.