mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

feat: Unfold widget

Open PatrickMassot opened this issue 2 years ago • 2 comments


Open in Gitpod

PatrickMassot avatar Nov 06 '23 00:11 PatrickMassot

please mark as awaiting-review if it's ready for review

fpvandoorn avatar Apr 05 '24 11:04 fpvandoorn

I hope this is superseded by #11768.

PatrickMassot avatar Apr 06 '24 14:04 PatrickMassot