mathlib3
5a61ec7d
- fix(scripts/add_port_comments): do not insert extra blank lines (#17850)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
fix(scripts/add_port_comments): do not insert extra blank lines (#17850) Since we insert the comment with a trailing newline, we should remove an extra newline when removing it.
Author
eric-wieser
Parents
d565b3df
Loading