Skip to content

[Merged by Bors] - chore(misc): fix whitespace#33004

Closed
harahu wants to merge 2 commits intoleanprover-community:masterfrom
harahu:chore/lint-misc-2
Closed

[Merged by Bors] - chore(misc): fix whitespace#33004
harahu wants to merge 2 commits intoleanprover-community:masterfrom
harahu:chore/lint-misc-2

Commits

Commits on Dec 17, 2025