Skip to content

Commit

Permalink
chore: more informative build message for figures (#96)
Browse files Browse the repository at this point in the history
Adds a more informative message while building figures (the generated
filenames) to make build traces easier to understand in CI.
  • Loading branch information
david-christiansen authored Oct 21, 2024
1 parent 0688dbd commit 532cd32
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,8 @@ target figures : Array FilePath := do
ensureDir "static"
ensureDir figureOutDir
for fmt in ["pdf", "svg"] do
IO.println s!"Format: {fmt}"
let built := s!"{f}.{fmt}"
IO.println s!"Generated: {figureOutDir.join built}"
IO.FS.withFile (figureDir.join built) .read fun h =>
IO.FS.withFile (figureOutDir.join built) .write fun h' => do
let mut buf ← h.read 1024
Expand Down

0 comments on commit 532cd32

Please sign in to comment.