Skip to content

Commit

Permalink
chore(category_theory/limits/shapes/concrete_category): Delete empty …
Browse files Browse the repository at this point in the history
…file (#18653)

This file was made empty in #9864 but not deleted.
  • Loading branch information
YaelDillies committed Mar 25, 2023
1 parent cb3ceec commit 0ca15f4
Showing 1 changed file with 0 additions and 20 deletions.
20 changes: 0 additions & 20 deletions src/category_theory/limits/shapes/concrete_category.lean

This file was deleted.

0 comments on commit 0ca15f4

Please sign in to comment.