Skip to content

[Merged by Bors] - chore(LongestPole): private an import to reduce the rebuild pole#39609

Closed
b-mehta wants to merge 6 commits into
leanprover-community:masterfrom
b-mehta:test-pole
Closed

[Merged by Bors] - chore(LongestPole): private an import to reduce the rebuild pole#39609
b-mehta wants to merge 6 commits into
leanprover-community:masterfrom
b-mehta:test-pole

alphabetize imports

626240c
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded May 22, 2026 in 1m 21s