mathlib3
448144f7 - chore(*): remove references to porting PRs (#18031)

Commit
3 years ago
chore(*): remove references to porting PRs (#18031) These no longer reflect the yaml file (which doesn't really track PR numbers any more). Since the next version of the bot will remove them, let's remove them manually first so that the bot diffs are easier to follow.
Author
Parents
Loading