mathlib3
[Merged by Bors] - refactor: redefine `bundle.total_space`
#19221

Closed

[Merged by Bors] - refactor: redefine `bundle.total_space` #19221

urkud wants to merge 12 commits into master from YK-bundle-fiber

Snapshot

d154f814

Don't start a second refactor here.

e2ec863e

github-actions added modifies-synchronized-file

Revert

a37cd8da

urkud added awaiting-review

urkud added mathport

Long lines

12bff639

Snapshot

23c592f7

Snapshot

e7ac51a1

Merge branch 'YK-simp-attrs' into YK-bundle-fiber

f29f5c5e

Fix merge

12b47e33

urkud requested a review 2 years ago

ghost added blocked-by-other-PR

Fix

a501c91c

Merge branch 'master' into YK-bundle-fiber

5614136f

ghost removed blocked-by-other-PR

Fix lint

15f3568f

Long line

1ec5c730

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~refactor: redefine `bundle.total_space`~~ [Merged by Bors] - refactor: redefine `bundle.total_space` 2 years ago

bors closed this 2 years ago

bors deleted the YK-bundle-fiber branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge mathport modifies-synchronized-file

Milestone

No milestone