From 532cd321ce537b9bd63ef895dd59373b6c7e57c1 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 21 Oct 2024 16:14:50 +0200 Subject: [PATCH] chore: more informative build message for figures (#96) Adds a more informative message while building figures (the generated filenames) to make build traces easier to understand in CI. --- lakefile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index 5fde1b4..1513bd0 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -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