diff --git a/lakefile.lean b/lakefile.lean
index 05906f7..80afa89 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -92,6 +92,18 @@ def getGitUrl (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String :
   let url := s!"{baseUrl}/blob/{commit}/{basePath}/{path}.lean"
   return url
 
+def runPdfLatex : BuildM PUnit := do
+  logInfo "Converting TeX to PDF"
+  let some docGen4 ← findPackage? `«doc-gen4»
+    | error "no doc-gen4 package found in workspace"
+  let pdfLatex := docGen4.srcDir / "run_pdflatex.sh"
+  let srcDir := (← getWorkspace).root.srcDir
+  let buildDir := (← getWorkspace).root.buildDir
+  proc {
+    cmd := pdfLatex.toString
+    args := #[srcDir.toString, buildDir.toString]
+  }
+
 module_facet docs (mod) : FilePath := do
   let some docGen4 ← findLeanExe? `«doc-gen4»
     | error "no doc-gen4 executable configuration found in workspace"
@@ -170,15 +182,7 @@ library_facet docs (lib) : FilePath := do
   coreJob.bindAsync fun _ coreInputTrace => do
     exeJob.bindAsync fun exeFile exeTrace => do
       moduleJobs.bindSync fun _ inputTrace => do
-        logInfo "Converting TeX to PDF"
-        let some docGen4 ← findPackage? `«doc-gen4»
-          | error "no doc-gen4 package found in workspace"
-        let pdfLatex := docGen4.srcDir / "run_pdflatex.sh"
-        let buildDir := (←getWorkspace).root.buildDir
-        proc {
-          cmd := pdfLatex.toString
-          args := #[buildDir.toString]
-        }
+        runPdfLatex
         let depTrace := mixTraceArray #[inputTrace, exeTrace, coreInputTrace]
         let trace ← buildFileUnlessUpToDate dataFile depTrace do
           logInfo "Documentation indexing"
diff --git a/run_pdflatex.sh b/run_pdflatex.sh
index b46f9cf..650c7ea 100755
--- a/run_pdflatex.sh
+++ b/run_pdflatex.sh
@@ -5,15 +5,20 @@ if ! command -v pdflatex > /dev/null; then
   exit 1
 fi
 
-BUILD_DIR="$1"
+SRC_DIR="$1"
+BUILD_DIR="$2"
+
+cd "$SRC_DIR" || (>&2 echo "Could not cd to $SRC_DIR"; exit 1)
 
 # We run this command twice to allow any cross-references to resolve correctly.
 # https://tex.stackexchange.com/questions/41539/does-hyperref-work-between-two-files
-TEX_FILES=$(find . -name ".tex" -not -path "*preamble.tex")
+TEX_FILES=$(find . -name "*.tex" -not -path "*preamble.tex")
 for _ in {1..2}; do
   for f in $TEX_FILES; do
     REL_DIR=$(dirname "$f")
-    REL_BASE=$(basename -s ".tex" "$1")
+    REL_BASE=$(basename -s ".tex" "$f")
+    mkdir -p "$BUILD_DIR/doc/$REL_DIR"
+    (cd "$REL_DIR" && pdflatex "$REL_BASE.tex")
     cp "$REL_DIR/$REL_BASE.pdf" "$BUILD_DIR/doc/$REL_DIR/"
   done
 done