Commit 2026-11-10 14:11 b679ac02

View on Github →

chore: remove trailing newlines in doc-strings (#45741) Per mathlib's style guide, module doc-strings are not supposed to end in a newline. About 3000 files in mathlib violate this. This also causes spurious diffs in the verso doc-string migration (see #45730). As a by-product, we also remove a few trailing newlines in other doc-strings. They need not be present either, and not removing them would be more work than it's worth. Also, the upcoming auto-formatter will most likely remove those anyway. This PR was generated purely mechanically by replacing the regex \n\n-/ with \n-/ within VS Code.

Estimated changes