mathlib
6dded232 - ci(bors): set update_base_for_deletes (#17410)

Commit
3 years ago
ci(bors): set update_base_for_deletes (#17410) From the source, this doesn't do anything to the git history, but does prevent chained PRs being closed after bors closes the first one. This still doesn't work very well for us, but it's better than randomly closing PRs that haven't been merged.
Author
Parents
Loading