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).
This commit is contained in:
parent
646f2fabbf
commit
6102f00322
1 changed files with 0 additions and 12 deletions
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue