mathlib
6d582e0f - fix(scripts/port_status): do not list sync-comment-only diffs (#17788)

Commit

3 years ago

fix(scripts/port_status): do not list sync-comment-only diffs (#17788) Tested by adding (and committing) a sync comment locally

Author

eric-wieser

Parents