Removed eigen mirror

phbasler · Oct 19, 2021 · 7071262 · 7071262
1 parent 8593ad3
commit 7071262
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 4 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -1,3 +0,0 @@
-[submodule "tools/eigen-git-mirror"]
-	path = tools/eigen-git-mirror
-	url = [email protected]:eigenteam/eigen-git-mirror.git

diff --git a/tools/eigen-git-mirror b/tools/eigen-git-mirror