mathlib3
11649045 - chore(scripts/port_status): reuse the parser from mathlibtools (#17620)

Commit

3 years ago

chore(scripts/port_status): reuse the parser from mathlibtools (#17620) This needs an unreleased version of mathlibtools.

Author

eric-wieser

Parents