Skip to content

Commit

Permalink
fix: remove white space
Browse files Browse the repository at this point in the history
  • Loading branch information
austinletson committed Jul 24, 2024
1 parent 2915bcd commit 8d664af
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion src/lake/Lake/CLI/Init.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 8d664af

Please sign in to comment.