mathlib3
[Merged by Bors] - chore(archive/imo): fix some naming inconsistencies and whitespace
#19155
Closed
Overview
Commits
1
Changes
View On GitHub

[Merged by Bors] - chore(archive/imo): fix some naming inconsistencies and whitespace #19155

adomani wants to merge 1 commit into master from adomani_imo_inconsistencies
adomani
adomani Fix some inconsistencies and whitespace
b3418094
adomani adomani added awaiting-CI
github-actions github-actions removed awaiting-CI
eric-wieser
eric-wieser commented on 2023-06-04
eric-wieser
eric-wieser approved these changes on 2023-06-04
bors
adomani
adomani
bors
bors bors changed the title chore(archive/imo): fix some naming inconsistencies and whitespace [Merged by Bors] - chore(archive/imo): fix some naming inconsistencies and whitespace 3 years ago
bors bors closed this 3 years ago
bors bors deleted the adomani_imo_inconsistencies branch 3 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
delegated
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum