diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 8f9749438614..5bad20a6f7f2 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -315,7 +315,6 @@ def validatePkgName (pkgName : String) : LogIO PUnit := do if pkgName.toLower ∈ ["init", "lean", "lake", "main"] then error "reserved package name" - def init (name : String) (tmp : InitTemplate) (lang : ConfigLang) (env : Lake.Env) (cwd : FilePath := ".") : LogIO PUnit := do let name ← id do if name == "." then