[Merged by Bors] - chore: remove fix-comments.py

[grunweg]

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.

---

Helps with #14539. PR #15222 (in progress) runs that script on all of mathlib, but is based on the above tag - removing it on master does not interfere with this.

[github-actions]

PR summary 41108bb85e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

- finish_comment():
- mktree(path,
- process_backticked_names(s):
- replace_names(s):

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for `script/declarations_diff.sh` contains some details about this script.

[j-loreaux]

I agree, now that the #aligns are actually removed, this has no use.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

[bryangingechen]

Thanks!
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style