From 3c033966e7bd0242eb7f554cf0ba90e28d6172fa Mon Sep 17 00:00:00 2001
From: Henrik <hargonix@gmail.com>
Date: Sun, 10 Sep 2023 11:47:36 +0200
Subject: [PATCH] feat: logStep in the facet to show progress

---
 lakefile.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index 48530a7..1eaa25a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -34,7 +34,7 @@ module_facet docs (mod) : FilePath := do
   modJob.bindSync fun _ modTrace => do
     let depTrace := exeTrace.mix modTrace
     let trace ← buildFileUnlessUpToDate docFile depTrace do
-      logInfo s!"Documenting module: {mod.name}"
+      logStep s!"Documenting module: {mod.name}"
       proc {
         cmd := exeFile.toString
         args := #["single", mod.name.toString]
@@ -51,7 +51,7 @@ target coreDocs : FilePath := do
   let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
   exeJob.bindSync fun exeFile exeTrace => do
     let trace ← buildFileUnlessUpToDate dataFile exeTrace do
-      logInfo "Documenting Lean core: Init and Lean"
+      logStep "Documenting Lean core: Init and Lean"
       proc {
         cmd := exeFile.toString
         args := #["genCore"]