[Merged by Bors] - chore(Tactic/Linter): unicode linter documentation improvements#38019
Closed
adomasbaliuka wants to merge 5 commits intoleanprover-community:masterfrom
Closed
[Merged by Bors] - chore(Tactic/Linter): unicode linter documentation improvements#38019adomasbaliuka wants to merge 5 commits intoleanprover-community:masterfrom
adomasbaliuka wants to merge 5 commits intoleanprover-community:masterfrom
Commits
Commits on Apr 13, 2026
Commits on Apr 14, 2026
- andauthored
- committed
- committed
- committed