Commit 2022-11-20 21:05 97f46ea9View on Github →
add_port_comments.py nightly (#17641)
Since this is modifying lean files and more could go wrong, this does not trigger bors automatically; but instead creates a PR for a human to double-check.
The PR description links to the mathlib4 PRs mentioned in the comments.
If a previous PR is open and not merged, this bot will update that PR. It remains to be seen how this will interact with bors.