Closed github-actions[bot] closed 1 year ago
Dunno if you @henryiii prefer to close this MR with conflicts and we pick up the updates the next round? I could also just edit by hand the updates in the new file post closing this.
Updates aren't necessary anymore, since the dev pages were the only place with these manual updates. (The site's pre-commit is separate)
Update the versions mentioned in the docs pages.
PR generated by "Update dependencies" workflow.