Commit 2026-02-17 14:20 ac6e2421

ci: add splice-bot action (#33979) Adds a CI action that inspects review comments. If a review comment posted by the PR author or a member of the reviewer or maintainer teams selects at least one line and contains the string splice-bot at the start of some line, then the bot will create a branch in the new mathlib4_copy repo with just the changes to the selected file, clearing all history, and then open a new PR from that branch. mathlib4_copy is a repo with GitHub actions disabled on it so that people cannot use SpliceBot to trigger workflows they otherwise couldn't. Reviewers and maintainers also have write permissions to mathlib4_copy so that they can make changes to the PR branches created by this bot if necessary. See https://github.com/leanprover-community/SpliceBot