mathlib3
a7aa4a2e - fix(scripts/port_comments): handle moved files (#17978)

Commit

3 years ago

fix(scripts/port_comments): handle moved files (#17978)

Author

eric-wieser

eric-wieser

Parents

Loading