From 5c40c1c7e6a3d5d606f3d7093e39422ee673ef79 Mon Sep 17 00:00:00 2001 From: acmepjz Date: Mon, 8 Jul 2024 02:25:01 +0800 Subject: [PATCH] fix build script --- lakefile.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index a8a1f223..123aa93a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -125,10 +125,10 @@ def getSrcUri (mod : Module) : IO String := do target bibPrepass : FilePath := do let exeJob ← «doc-gen4».fetch - let basePath := (←getWorkspace).root.buildDir / "doc" - let inputJsonFile := (←getWorkspace).root.srcDir / "docs" / "references.json" - let inputBibFile := (←getWorkspace).root.srcDir / "docs" / "references.bib" - let outputFile := basePath / "declarations" / "references.json" + let dataPath := (← getWorkspace).root.buildDir / "doc-data" + let inputJsonFile := (← getWorkspace).root.srcDir / "docs" / "references.json" + let inputBibFile := (← getWorkspace).root.srcDir / "docs" / "references.bib" + let outputFile := dataPath / "references.json" let tryJson : JobM (Array String × BuildTrace) := do let inputTrace ← mixTrace (BuildTrace.ofHash (.ofString "json")) <$> computeTrace inputJsonFile pure (#["--json", inputJsonFile.toString], inputTrace)