Public Service Announcement: There is a GitHub action that lets you automatically label PRs based on what paths they modify.
https://github.com/actions/labeler If we set this up, perhaps down the line we can update the PR dashboard and PR merge script to use the tags. cc @Dongjoon Hyun <[email protected]>, who may be interested in this. Nick
