#!/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 "" >> gifs.html echo "" >> gifs.html echo "CGAL Manual gif test for directory $SUBDIR" >> gifs.html echo "" >> gifs.html echo "" >> gifs.html grep -n '.gif' $HTML_FILES >> gifs.html echo "" >> gifs.html echo "" >> 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 "
  • $DIR" >> ../gif_grep_list.html SUBDIRS=`ls` # grep for gifs in all subdirectories echo "" >> ../gif_grep_list.html } print_header() { echo "" >> gif_grep_list.html echo "" >> gif_grep_list.html echo "CGAL Manual gif test" >> gif_grep_list.html echo "" >> gif_grep_list.html echo "" >> 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 "

    " >> gif_grep_list.html echo "

    " >> gif_grep_list.html echo "" >> gif_grep_list.html echo "" >> 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