scripts/rewrap-comments.py: rewrap comments without a metamath build - #5456

Open

vince-gonzalez wants to merge 4 commits into

metamath:developfrom

vince-gonzalez:rewrap-comments

Commits on Aug 23, 2026

scripts: rewrap comments without the metamath program
vince-gonzalez
committed
d608822

Commits on Aug 24, 2026

scripts/rewrap-comments.py: author line, and skip file inclusions
vince-gonzalez
committed
b75ff96
scripts/rewrap-comments.py: note the inclusion difference, name the executable
vince-gonzalez
committed
1daa54c

Commits on Sep 8, 2026

scripts/rewrap-comments.py: document why COMMENT ends at the first $)
vince-gonzalez
committed
368e9f2