tree 1cc00669efd9700af078635b49550a96b4220509
parent d90707d363a83e73b7ec715fa61a6e20b054ca0d
author Chi Wang <chiwang@google.com> 1695634877 +0200
committer GitHub <noreply@github.com> 1695634877 +0200
gpgsig -----BEGIN PGP SIGNATURE-----
 
 wsBcBAABCAAQBQJlEVW9CRBK7hj4Ov3rIwAAbfoIAKq1IPvGjHqw3VCHbOKJ6G7Q
 EjlqYrjOyRym0nQePwSJdvWKAOvCVhE7dqu4gI0F5Lhl9RJn8gzVISBUzUPdjyXF
 IeIp5b5kBOANYSfxZK9jZKoumrBVihiH53lJOjwkiG3N+y+Z5N5fOERCeiZCoFG+
 QevZHgIOujw/BMjvVV07dTDy+e+WXgnR++fhstH8okneNZaD8HsKIpDEEXbaxdal
 v/sWv26ZyjhXnbzEDG1RhTHtzEyvL+aeOGteeOWs7cStGAXTK4eTIvIA/FHtispi
 PaIDsCe+5Wgx+aLzrZkEf2GtGD2mwVLryVXqrqNwMlYGpz3cRsrpyRwYn5ttKfk=
 =gnXJ
 -----END PGP SIGNATURE-----
 

Update dashboard (#1743)

Check in bunch of fixes/updates:

- Sort repo by names when displaying them on the sidebar.
- Use JDK20.
- Remove duplicated `team_owner` field in `github_team_table`. Make it
easier to change owners of repo.
- Use case-insensitive text for labels to match the search result on
Github.
- Fix a bug that sometimes action owners for an issue are not correctly
computed.
- Update the logic for determining whether an issue/PR is triaged
according to today's triaging process.
- Update nagging emails to have a separated PRs section.
- Improve sync process.

Fixes #1732.