summaryrefslogtreecommitdiff
path: root/maintainer-scripts
diff options
context:
space:
mode:
authorGerald Pfeifer <gerald@pfeifer.com>2013-12-02 20:07:14 +0000
committerGerald Pfeifer <gerald@gcc.gnu.org>2013-12-02 20:07:14 +0000
commit52cacf7207de329a48b63f1a4cf1cb3cef37fdea (patch)
treeef796b29099fe7224826e94c12f2f25490b2b0d4 /maintainer-scripts
parentb6cfa9eb37ce4234a032dd0d8363b8d22334e739 (diff)
downloadgcc-52cacf7207de329a48b63f1a4cf1cb3cef37fdea.tar.gz
update_web_docs_svn: Work around makeinfo generated file names and references with "_002d" instead...
* update_web_docs_svn: Work around makeinfo generated file names and references with "_002d" instead of "-". From-SVN: r205600
Diffstat (limited to 'maintainer-scripts')
-rw-r--r--maintainer-scripts/ChangeLog5
-rwxr-xr-xmaintainer-scripts/update_web_docs_svn13
2 files changed, 18 insertions, 0 deletions
diff --git a/maintainer-scripts/ChangeLog b/maintainer-scripts/ChangeLog
index 8f18264fa6c..867d0ca4771 100644
--- a/maintainer-scripts/ChangeLog
+++ b/maintainer-scripts/ChangeLog
@@ -1,3 +1,8 @@
+2013-12-02 Gerald Pfeifer <gerald@pfeifer.com>
+
+ * update_web_docs_svn: Work around makeinfo generated file names
+ and references with "_002d" instead of "-".
+
2013-04-12 Jakub Jelinek <jakub@redhat.com>
* crontab: Disable snapshots from gcc-4_6-branch.
diff --git a/maintainer-scripts/update_web_docs_svn b/maintainer-scripts/update_web_docs_svn
index cfc33c42bf5..8a5883eeca7 100755
--- a/maintainer-scripts/update_web_docs_svn
+++ b/maintainer-scripts/update_web_docs_svn
@@ -172,6 +172,19 @@ for file in $MANUALS; do
fi
done
+# Work around makeinfo generated file names and references with
+# "_002d" instead of "-".
+find . -name '*.html' | while read f; do
+ # Do this for the contents of each file.
+ sed -i -e 's/_002d/-/g' "$f"
+ # And rename files if necessary.
+ ff=`echo $f | sed -e 's/_002d/-/g'`;
+ if [ "$f" != "$ff" ]; then
+ printf "Renaming %s to %s\n" "$f" "$ff"
+ mv "$f" "$ff"
+ fi
+done
+
# Then build a gzipped copy of each of the resulting .html, .ps and .tar files
for file in */*.html *.ps *.pdf *.tar; do
cat $file | gzip --best > $file.gz