From 36813f7d8d1e46f92676f06a0f977170729fdbed Mon Sep 17 00:00:00 2001
From: jsm28 <jsm28@138bc75d-0d04-0410-961f-82ee72b054a4>
Date: Fri, 30 Sep 2005 22:06:07 +0000
Subject: [PATCH] 	PR other/23693 	* update_web_docs: Add PDF support. 
 Correct check of DEV-PHASE.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@104837 138bc75d-0d04-0410-961f-82ee72b054a4
---
 maintainer-scripts/ChangeLog       | 5 +++++
 maintainer-scripts/update_web_docs | 9 +++++----
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/maintainer-scripts/ChangeLog b/maintainer-scripts/ChangeLog
index d2f15850040..24e51deb9fd 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 d7b3da116fd..6c14c68b070 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
-- 
2.11.0