Closed faenuccio closed 4 months ago
I don't know!
I don't know!
Perhaps @fpvandoorn knows, or knows who to ping? It seems that the PR process on this repo is harder than on mathlib... 😓 .
I or another maintainer presses squash and merge
:-)
@YaelDillies , what should happen after you "approved" these changes (and those of #440 )?