mathlib

314d3a57 - fix(scripts/port_status): fix `--ignore-matching-lines` arguments (#17865)

fix(scripts/port_status): fix `--ignore-matching-lines` arguments (#17865) It turns out that in `--name-only` mode these arguments are ignored. It also turns out that the regex that was in this Python script did not work. Thankfully these errors conspired together, meaning that ultimately #17788 was mostly a no-op (except on old versions of git, where it stopped working entirely)