Skip to content

[Merged by Bors] - fix: shake the import tree#9749

Closed
urkud wants to merge 1 commit intomasterfrom
YK-shake-apply
Closed

[Merged by Bors] - fix: shake the import tree#9749
urkud wants to merge 1 commit intomasterfrom
YK-shake-apply

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Jan 14, 2024

cherry-picked from #9347

Co-Authored-By: @digama0


Open in Gitpod

cherry-picked from #9347
@urkud urkud mentioned this pull request Jan 14, 2024
1 task
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jan 15, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jan 15, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 15, 2024
cherry-picked from #9347

Co-Authored-By: @digama0
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 15, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix: shake the import tree [Merged by Bors] - fix: shake the import tree Jan 15, 2024
@mathlib-bors mathlib-bors bot closed this Jan 15, 2024
@mathlib-bors mathlib-bors bot deleted the YK-shake-apply branch January 15, 2024 01:46
linesthatinterlace pushed a commit that referenced this pull request Jan 16, 2024
cherry-picked from #9347

Co-Authored-By: @digama0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants