mathlib3
d82d6e26 - chore(*): add mathlib3 synchronization labels (#17314)

Commit

3 years ago

chore(*): add mathlib3 synchronization labels (#17314) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents