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 <dongjoon.h...@gmail.com>, who may be interested in this. Nick
