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.
20 files changed
