From 9a3657df3fe105a3d9cee172caa0495583f71f4f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 17 Mar 2023 11:18:39 +0100 Subject: [PATCH] chore: remove Lake submodule --- .gitmodules | 4 ---- src/lake | 1 - 2 files changed, 5 deletions(-) delete mode 100644 .gitmodules delete mode 160000 src/lake diff --git a/.gitmodules b/.gitmodules deleted file mode 100644 index 60b7cc5409..0000000000 --- a/.gitmodules +++ /dev/null @@ -1,4 +0,0 @@ -[submodule "lake"] - path = src/lake - url = https://github.com/leanprover/lake.git - ignore = untracked \ No newline at end of file diff --git a/src/lake b/src/lake deleted file mode 160000 index 9919b5efc4..0000000000 --- a/src/lake +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 9919b5efc48c71a940635a0bbab00a394ebe53f8