From: Ben Pfaff <blp@cs.stanford.edu>
Date: Tue, 1 Dec 2020 06:43:26 +0000 (-0800)
Subject: build-pspp: Fix documentation build.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=7036cc841d028475016f848ef49a2e7d7fc04edb;p=pspp

build-pspp: Fix documentation build.
---

diff --git a/build-pspp b/build-pspp
index 7cc875656b..83f5d1aa71 100755
--- a/build-pspp
+++ b/build-pspp
@@ -434,14 +434,13 @@ Changes from %(repo_version)s to %(version)s:
 
     # Build examples for user manual.
     start_step("Build examples for user manual")
-    run("cd pspp/_build && make -j$(nproc) example-outputs example-html")
+    run("cd pspp/_build && make -j$(nproc) figure-spvs figure-txts figure-texis figure-htmls")
 
     # Build user manual
     start_step("Build user manual")
     run("cd pspp && "
         "GENDOCS_TEMPLATE_DIR=%s %s/gendocs.sh -s doc/pspp.texi -I doc "
-        "-I _build/doc/examples -I doc/examples "
-        "-o %s/user-manual --email bug-gnu-pspp@gnu.org "
+        "-I _build/doc -o %s/user-manual --email bug-gnu-pspp@gnu.org "
         "pspp \"GNU PSPP User Manual\"" % (topdir, topdir, resultsdir),
         "user-manual")
     saved_result("User Manual", "user-manual")