feat: logStep in the facet to show progress
parent
a090875215
commit
3c033966e7
|
@ -34,7 +34,7 @@ module_facet docs (mod) : FilePath := do
|
||||||
modJob.bindSync fun _ modTrace => do
|
modJob.bindSync fun _ modTrace => do
|
||||||
let depTrace := exeTrace.mix modTrace
|
let depTrace := exeTrace.mix modTrace
|
||||||
let trace ← buildFileUnlessUpToDate docFile depTrace do
|
let trace ← buildFileUnlessUpToDate docFile depTrace do
|
||||||
logInfo s!"Documenting module: {mod.name}"
|
logStep s!"Documenting module: {mod.name}"
|
||||||
proc {
|
proc {
|
||||||
cmd := exeFile.toString
|
cmd := exeFile.toString
|
||||||
args := #["single", mod.name.toString]
|
args := #["single", mod.name.toString]
|
||||||
|
@ -51,7 +51,7 @@ target coreDocs : FilePath := do
|
||||||
let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
|
let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
|
||||||
exeJob.bindSync fun exeFile exeTrace => do
|
exeJob.bindSync fun exeFile exeTrace => do
|
||||||
let trace ← buildFileUnlessUpToDate dataFile exeTrace do
|
let trace ← buildFileUnlessUpToDate dataFile exeTrace do
|
||||||
logInfo "Documenting Lean core: Init and Lean"
|
logStep "Documenting Lean core: Init and Lean"
|
||||||
proc {
|
proc {
|
||||||
cmd := exeFile.toString
|
cmd := exeFile.toString
|
||||||
args := #["genCore"]
|
args := #["genCore"]
|
||||||
|
|
Loading…
Reference in New Issue