fix build script

leanprover · Jul 7, 2024 · 5c40c1c · 5c40c1c
1 parent 2001dbb
commit 5c40c1c
Showing 1 changed file with 4 additions and 4 deletions.
diff --git 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)