mathlib3
chore(data/list/basic): rename take_all -> take_length
#2343
Merged
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Overview
Commits
4
Changes
View On
GitHub
chore(data/list/basic): rename take_all -> take_length
#2343
mergify
merged 4 commits into
master
from
rename_take_all
chore(data/list/basic): rename take_all -> take_length
b5743726
also rename drop_all
8602959b
cipher1024
approved these changes on 2020-04-07
cipher1024
added
ready-to-merge
Merge branch 'master' into rename_take_all
4ee10d40
Merge branch 'master' into rename_take_all
b271f1a6
mergify
merged
2f2e016e
into master
5 years ago
mergify
deleted the rename_take_all branch
5 years ago
Login to write a write a comment.
Login via GitHub
Reviewers
cipher1024
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub