chore: ignore more revisions in .git-blame-ignore-revs (#41681)

grunweg · grunweg · commit 119eea4bbfa6 · 2026-07-17T09:57:55.000Z
There are surely more such PRs, but I won't hunt them all down. Having a way to sort such PRs by diff (and tackling the largest PRs first) would be nice.
diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
@@ -4,3 +4,5 @@
 fc48848e4374f13c796a7399bfccd2e228f776df
 # 2025-11-19 move Mathlib to the module system (#31786)
 6a54a80825b060ab20dc31751ebdce78b3a3b518
+# 2025-12-01 fix spelling in doc-strings (#32286)
+b728e1450a53133aa4171eeadc0bc8d3ee58415c
