Reverted delete

phbasler · Oct 19, 2021 · 8593ad3 · 8593ad3
1 parent 702bc95
commit 8593ad3
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "tools/eigen-git-mirror"]
+	path = tools/eigen-git-mirror
+	url = [email protected]:eigenteam/eigen-git-mirror.git