From dc3e1bf0d7e692781ccd0a1a132f5d62c95b17f9 Mon Sep 17 00:00:00 2001 From: Austin Letson Date: Wed, 24 Jul 2024 17:38:13 -0400 Subject: [PATCH] fix: `logInfo` -> `logVerbose` Co-authored-by: Mac Malone --- src/lake/Lake/CLI/Init.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 6b9f3307a749..b2169aad3341 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -308,11 +308,11 @@ def createLeanActionWorkflow (dir : FilePath) : LogIO PUnit := do let workflowDir := dir / ".github" / "workflows" let workflowFile := workflowDir / "lean_action_ci.yml" if (← workflowFile.pathExists) then - logWarning "lean-action CI workflow already exists" + logVerbose "lean-action CI workflow already exists" return IO.FS.createDirAll workflowDir IO.FS.writeFile workflowFile leanActionWorkflowContents - logInfo s!"created lean-action CI workflow at '{workflowFile}'" + logVerbose s!"created lean-action CI workflow at '{workflowFile}'" def init (name : String) (tmp : InitTemplate) (lang : ConfigLang) (env : Lake.Env) (cwd : FilePath := ".") : LogIO PUnit := do let name ← id do