mathlib

2da281a1 - fix(scripts/add_port_comments): do not add PR numbers to port comments (#18030)

fix(scripts/add_port_comments): do not add PR numbers to port comments (#18030) The now-automated port status YAML file no longer contains accurate PR numbers; many refer to ad-hoc ports rather than the real port. Since the PR numbers can no longer be trusted, we just omit them; both from the comment and the bot's commit message.