Tobias Henkel 808db0aec9 Report max 50 file comments to github ... The github api limits us to report 50 file comments per api request. Since the check run reporting is in the critical path don't do paging but limit this to 50 comments. In order to get a diverse feedback sort the messages by 'uniqueness' first so that 100 equal comments don't push out 5 other comments that are valuable. Change-Id: If5a7c246a58b510d8fcfa31bd71d74c84acbc278		2021-03-15 15:49:24 -07:00
..
git	Report max 50 file comments to github	2021-03-15 15:49:24 -07:00
main.yaml	Support file comments via Github checks API	2020-02-19 14:01:41 +01:00