From 6a82a28a50a576a95355cb0917a02b501646f652 Mon Sep 17 00:00:00 2001
From: Joseph Myers <joseph@codesourcery.com>
Date: Fri, 30 Sep 2005 23:06:07 +0100
Subject: re PR other/23693 (Manuals in the  Portable Document Format (PDF))

	PR other/23693
	* update_web_docs: Add PDF support.  Correct check of DEV-PHASE.

From-SVN: r104837
---
 maintainer-scripts/ChangeLog       | 5 +++++
 maintainer-scripts/update_web_docs | 9 +++++----
 2 files changed, 10 insertions(+), 4 deletions(-)

(limited to 'maintainer-scripts')

diff --git a/maintainer-scripts/ChangeLog b/maintainer-scripts/ChangeLog
index d2f1585..24e51de 100644
--- a/maintainer-scripts/ChangeLog
+++ b/maintainer-scripts/ChangeLog
@@ -1,5 +1,10 @@
 2005-09-30  Joseph S. Myers  <joseph@codesourcery.com>
 
+	PR other/23693
+	* update_web_docs: Add PDF support.  Correct check of DEV-PHASE.
+
+2005-09-30  Joseph S. Myers  <joseph@codesourcery.com>
+
 	* update_web_docs_old: Remove.
 
 2005-08-14  Kelley Cook  <kcook@gcc.gnu.org>
diff --git a/maintainer-scripts/update_web_docs b/maintainer-scripts/update_web_docs
index d7b3da1..6c14c68 100755
--- a/maintainer-scripts/update_web_docs
+++ b/maintainer-scripts/update_web_docs
@@ -110,26 +110,27 @@ fi
 # Generate gcc-vers.texi.
 (
    echo "@set version-GCC $(cat gcc/gcc/BASE-VER)"
-   if "$(cat gcc/gcc/DEV-PHASE)" = "experimental"; then
+   if [ "$(cat gcc/gcc/DEV-PHASE)" = "experimental" ]; then
       echo "@set DEVELOPMENT"
    else
       echo "@clear DEVELOPMENT"
    fi
 ) > $includedir/gcc-vers.texi
 
-# Now convert the relevant files from texi to HTML and PostScript.
+# Now convert the relevant files from texi to HTML, PDF and PostScript.
 for file in $MANUALS; do
   filename=`find . -name ${file}.texi`
   if [ "${filename}" ]; then
     makeinfo --html -I ${includedir} -I `dirname ${filename}` ${filename}
     tar cf ${file}-html.tar ${file}/*.html
     texi2dvi -I ${includedir} ${filename} </dev/null && dvips -o ${file}.ps ${file}.dvi
+    texi2pdf -I ${includedir} ${filename} </dev/null
     mkdir -p $DOCSDIR/$file
   fi
 done
 
 # Then build a gzipped copy of each of the resulting .html, .ps and .tar files
-for file in */*.html *.ps *.tar; do
+for file in */*.html *.ps *.pdf *.tar; do
   cat $file | gzip --best > $file.gz
 done
 
@@ -144,7 +145,7 @@ if test $today = 15; then
 fi
 
 # And copy the resulting files to the web server
-for file in */*.html *.ps *.tar; do
+for file in */*.html *.ps *.pdf *.tar; do
   cat $DOCSDIR/$file | 
     sed -e '/^<meta name=generator/d' \
         -e '/^%DVIPSSource:/d' > file1
-- 
cgit v1.1