Skip to content

fix: replace dropRightWhile with dropEndWhile#264

Open
Neptunium931 wants to merge 1 commit into
leanprover:masterfrom
Neptunium931:dropRightWhile/deprecated
Open

fix: replace dropRightWhile with dropEndWhile#264
Neptunium931 wants to merge 1 commit into
leanprover:masterfrom
Neptunium931:dropRightWhile/deprecated

fix: replace dropRightWhile with dropEndWhile

e00aff6
Select commit
Loading
Failed to load commit list.

Workflow runs completed with no jobs