These are not run in CI since #2353 and are likely to go out of date. If we want a script that users can run locally then we should create a new script that wraps our current CI.
Rather than modifying the labels manually, which we often forget, we can label the PRs automatically. This will make it easier to search PRs.