From 6102f003227f6b5a8f383948e1dce83cc09fd789 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Fri, 26 Sep 2025 16:51:02 -0400
Subject: [PATCH] chore: rm `src/lake/lakefile.toml` (#10580)

This file is essentially just for me and can cause problems with the
language server, so I have removed it from the committed code (and left
an ignored version on my own setup).
---
 src/lake/lakefile.toml | 12 ------------
 1 file changed, 12 deletions(-)
 delete mode 100644 src/lake/lakefile.toml

diff --git a/src/lake/lakefile.toml b/src/lake/lakefile.toml
deleted file mode 100644
index 39a2513458..0000000000
--- a/src/lake/lakefile.toml
+++ /dev/null
@@ -1,12 +0,0 @@
-name = "lake"
-defaultTargets = ["Lake", "lake"]
-
-[[lean_lib]]
-name = "Lake"
-defaultFacets = ["shared"]
-
-[[lean_exe]]
-name = "lake"
-root = "LakeMain"
-supportInterpreter = true
-leanOptions.experimental.module = true