Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This has been disabled for a month now, and it doesn't seem like we missed it too much. I think it's safe to remove this now. Also, now that we no longer attempt to merge approved pull requests at regular intervals, there is no need to dismiss approvals from PRs when this workflow fails. Presumably this was needed to avoid the workflow from repeatedly attempting to publish a PR that cannot be published, but this no longer a concern.
- Loading branch information