fix: more logInfo -> logVerbose

leanprover · Jul 24, 2024 · ada5032 · ada5032
1 parent dc3e1bf
commit ada5032
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean
@@ -304,7 +304,7 @@ def validatePkgName (pkgName : String) : LogIO PUnit := do
     error "reserved package name"
 
 def createLeanActionWorkflow (dir : FilePath) : LogIO PUnit := do
-  logInfo "creating lean-action CI workflow"
+  logVerbose "creating lean-action CI workflow"
   let workflowDir := dir / ".github" / "workflows"
   let workflowFile := workflowDir / "lean_action_ci.yml"
   if (← workflowFile.pathExists) then