Commit 53fd774
chore(OpenPartialHomeomorph): add missing deprecation (leanprover-community#39968)
Add deprecation that I forgot in leanprover-community#39565.
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>1 parent 2d92fbb commit 53fd774
1 file changed
Lines changed: 2 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
167 | 167 | | |
168 | 168 | | |
169 | 169 | | |
| 170 | + | |
| 171 | + | |
170 | 172 | | |
171 | 173 | | |
172 | 174 | | |
| |||
0 commit comments