1000th

Stream: general

[Patrick Massot]

Mario and Johannes, do you have any idea what should be the 1000th commit to mathlib? It may come very soon, especially since the module refactor is now PR'ed and we have that Freiburg meeting coming.