mathlib3
99c3e223 - refactor(geometry/manifold): remove old_structure_cmd (#9617)

Commit

4 years ago

refactor(geometry/manifold): remove old_structure_cmd (#9617) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents