From: Ben Pfaff <blp@cs.stanford.edu>
Date: Fri, 11 Jan 2013 16:50:02 +0000 (-0800)
Subject: build-pspp: Use -I flag to newer gendocs.sh to copy HTML image files.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=674fd625303321472d4fa89a6d1d62058790b87e;p=pspp

build-pspp: Use -I flag to newer gendocs.sh to copy HTML image files.

The image files were being omitted from the HTML version of the generated
manual.  Using -I with sufficiently newer gendocs.sh solves the problem.

Reported by John Darrington.
---

diff --git a/build-pspp b/build-pspp
index ae723f7de4..6c1a30dc9b 100755
--- a/build-pspp
+++ b/build-pspp
@@ -268,13 +268,12 @@ EOF
 
     # Build user manual
     start_step ("Build user manual");
-    run ("cd pspp && cp _build/doc/*.texi doc/");
-    run ("cd pspp && GENDOCS_TEMPLATE_DIR=$topdir $topdir/gendocs.sh -s doc/pspp.texinfo -o $resultsdir/user-manual --email bug-gnu-pspp\@gnu.org pspp \"GNU PSPP User Manual\"", "user-manual");
+    run ("cd pspp && GENDOCS_TEMPLATE_DIR=$topdir $topdir/gendocs.sh -s doc/pspp.texinfo -I doc -o $resultsdir/user-manual --email bug-gnu-pspp\@gnu.org pspp \"GNU PSPP User Manual\"", "user-manual");
     saved_result ("User Manual", "user-manual");
 
     # Build developer's guide
     start_step ("Build developers guide");
-    run ("cd pspp && GENDOCS_TEMPLATE_DIR=$topdir $topdir/gendocs.sh -s doc/pspp-dev.texinfo -o $resultsdir/dev-guide --email bug-gnu-pspp\@gnu.org pspp-dev \"GNU PSPP Developers Guide\"", "dev-guide");
+    run ("cd pspp && GENDOCS_TEMPLATE_DIR=$topdir $topdir/gendocs.sh -s doc/pspp-dev.texinfo -I doc -o $resultsdir/dev-guide --email bug-gnu-pspp\@gnu.org pspp-dev \"GNU PSPP Developers Guide\"", "dev-guide");
     saved_result ("Developers Guide", "dev-guide");
 } else {
     $tarball = saved_result ("source distribution", $tarball);