mathlib3
f2f23df7 - ci(scripts/add_port_comments): deal with files that have no module docstring to edit (#17737)

Commit

3 years ago

ci(scripts/add_port_comments): deal with files that have no module docstring to edit (#17737) The action on `master` was crashing due to a missing module docstring

Author

eric-wieser

Parents

a148d797

mathlib3 f2f23df7 - ci(scripts/add_port_comments): deal with files that have no module docstring to edit (#17737)

mathlib3
f2f23df7 - ci(scripts/add_port_comments): deal with files that have no module docstring to edit (#17737)