Fix typo: Use en dash for separating names: Escardó–Simpson instead of Escardó-Simpson #1185
Merged
mikeshulman merged 1 commit intoHoTT:masterfrom Jul 3, 2025
Merged
Fix typo: Use en dash for separating names: Escardó–Simpson instead of Escardó-Simpson #1185mikeshulman merged 1 commit intoHoTT:masterfrom
mikeshulman merged 1 commit intoHoTT:masterfrom
Commits
Commits on Jul 1, 2025
- committed
Quirin Schroll