mirror of https://github.com/CGAL/cgal
101 lines
2.9 KiB
Bash
Executable File
101 lines
2.9 KiB
Bash
Executable File
#!/bin/sh
|
|
#
|
|
# Purpose: Used to check if the pictures (gif files) linked in the manual
|
|
# are in their proper places. Creates a web page that contains
|
|
# the result of a grep for "gif" in each html file. In most
|
|
# cases, this grep provides enough information so the page contains
|
|
# simply pictures or "broken picture" icons.
|
|
#
|
|
# Usage: gif_grep [d1 d2 ...]
|
|
#
|
|
# If no argument is given, the default is to grep all html files
|
|
# in the current directory and all subdirectories. Otherwise,
|
|
# only the html files in subdirectories given as arguments are
|
|
# searched.
|
|
|
|
|
|
\rm -f gif_grep_list.html
|
|
if [ $# -ne 0 ] ; then
|
|
CONTENTS="$*"
|
|
else
|
|
CONTENTS=`ls`
|
|
fi
|
|
|
|
|
|
make_gif_grep_file()
|
|
{
|
|
\rm -f gifs.html
|
|
HTML_FILES=`ls *.html`
|
|
|
|
touch gifs.html
|
|
if [ "$HTML_FILES" != "" ]; then
|
|
echo "<HTML>" >> gifs.html
|
|
echo "<HEAD>" >> gifs.html
|
|
echo "<TITLE>CGAL Manual gif test for directory $SUBDIR</TITLE>" >> gifs.html
|
|
echo "</HEAD>" >> gifs.html
|
|
echo "<BODY>" >> gifs.html
|
|
grep -n '.gif' $HTML_FILES >> gifs.html
|
|
echo "</BODY>" >> gifs.html
|
|
echo "</HTML>" >> gifs.html
|
|
else
|
|
echo "No HTML files in directory $SUBDIR" >> gifs.html
|
|
fi
|
|
}
|
|
|
|
create_gif_grep_list()
|
|
{
|
|
\rm -f gif_grep_list.html
|
|
# grep for gifs in the current directory
|
|
make_gif_grep_file
|
|
echo "<LI><A HREF=\"$DIR/gifs.html\">$DIR</A>" >> ../gif_grep_list.html
|
|
SUBDIRS=`ls`
|
|
# grep for gifs in all subdirectories
|
|
echo "<UL>" >> ../gif_grep_list.html
|
|
for SUBDIR in $SUBDIRS ; do
|
|
if [ -d $SUBDIR -a $SUBDIR != "gif" ]; then
|
|
echo "<LI><A HREF=\"$DIR/$SUBDIR/gifs.html\">$SUBDIR</A>" >> ../gif_grep_list.html
|
|
cd $SUBDIR
|
|
# echo "Now in directory $SUBDIR"
|
|
make_gif_grep_file
|
|
# echo "Leaving directory $SUBDIR"
|
|
cd ..
|
|
fi
|
|
done
|
|
echo "</UL>" >> ../gif_grep_list.html
|
|
}
|
|
|
|
print_header()
|
|
{
|
|
echo "<HTML>" >> gif_grep_list.html
|
|
echo "<HEAD>" >> gif_grep_list.html
|
|
echo "<TITLE>CGAL Manual gif test</TITLE>" >> gif_grep_list.html
|
|
echo "</HEAD>" >> gif_grep_list.html
|
|
echo "<BODY>" >> gif_grep_list.html
|
|
echo "Follow the links below to reach the pages corresponding to the results">> gif_grep_list.html
|
|
echo "of the grep for \"gif\" in the html files of each directory." >> gif_grep_list.html
|
|
echo "\"Broken picture\" icons may indicate the absence of the referenced" >> gif_grep_list.html
|
|
echo "gif file." >> gif_grep_list.html
|
|
echo "<P>" >> gif_grep_list.html
|
|
echo "<UL>" >> gif_grep_list.html
|
|
}
|
|
|
|
print_footer()
|
|
{
|
|
echo "</UL>" >> gif_grep_list.html
|
|
echo "</BODY>" >> gif_grep_list.html
|
|
echo "</HTML>" >> gif_grep_list.html
|
|
}
|
|
|
|
print_header
|
|
for DIR in $CONTENTS; do
|
|
if [ -d $DIR ]; then
|
|
cd $DIR
|
|
# echo "in directory $DIR"
|
|
create_gif_grep_list
|
|
# echo "leaving directory $DIR"
|
|
cd ..
|
|
fi
|
|
done
|
|
print_footer
|
|
|