mirror of git://gcc.gnu.org/git/gcc.git
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
This commit is contained in:
parent
b6cfa9eb37
commit
52cacf7207
|
|
@ -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>
|
2013-04-12 Jakub Jelinek <jakub@redhat.com>
|
||||||
|
|
||||||
* crontab: Disable snapshots from gcc-4_6-branch.
|
* crontab: Disable snapshots from gcc-4_6-branch.
|
||||||
|
|
|
||||||
|
|
@ -172,6 +172,19 @@ for file in $MANUALS; do
|
||||||
fi
|
fi
|
||||||
done
|
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
|
# Then build a gzipped copy of each of the resulting .html, .ps and .tar files
|
||||||
for file in */*.html *.ps *.pdf *.tar; do
|
for file in */*.html *.ps *.pdf *.tar; do
|
||||||
cat $file | gzip --best > $file.gz
|
cat $file | gzip --best > $file.gz
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue