Commit 2022-11-20 21:05 97f46ea9

View on Github →

ci: run 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.

Estimated changes