From a344c1b2ea11c3bfeeb391279001c857b2fedfb7 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 1 Aug 2024 12:30:11 -0400
Subject: [PATCH] Drop an empty file

We can recreate it later, if needed.
---
 SphereEversion.lean                         | 1 -
 SphereEversion/ToMathlib/Topology/Germ.lean | 2 --
 2 files changed, 3 deletions(-)
 delete mode 100644 SphereEversion/ToMathlib/Topology/Germ.lean

diff --git a/SphereEversion.lean b/SphereEversion.lean
index 1419c40e..dfa89056 100644
--- a/SphereEversion.lean
+++ b/SphereEversion.lean
@@ -60,7 +60,6 @@ import SphereEversion.ToMathlib.Order.Filter.Basic
 import SphereEversion.ToMathlib.Partition
 import SphereEversion.ToMathlib.SmoothBarycentric
 import SphereEversion.ToMathlib.Topology.Algebra.Module
-import SphereEversion.ToMathlib.Topology.Germ
 import SphereEversion.ToMathlib.Topology.HausdorffDistance
 import SphereEversion.ToMathlib.Topology.Misc
 import SphereEversion.ToMathlib.Topology.Paracompact
diff --git a/SphereEversion/ToMathlib/Topology/Germ.lean b/SphereEversion/ToMathlib/Topology/Germ.lean
deleted file mode 100644
index a02e2ec7..00000000
--- a/SphereEversion/ToMathlib/Topology/Germ.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-import Mathlib.Topology.Germ
--- leaving this file blank, for future PRs moving material here