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