Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: remove fix-comments.py (#15242)
This script has served its purpose during the port; now that all align information has been removed from mathlib, it is not useful for other projects either. Projects which wish to use such functionality should check out the v3-eol tag and use the script from that commit.
- Loading branch information