equal
deleted
inserted
replaced
147 echo "###" |
147 echo "###" |
148 |
148 |
149 cd "$DISTBASE/$DISTNAME/Doc" |
149 cd "$DISTBASE/$DISTNAME/Doc" |
150 PDFLATEX=$(type -path pdflatex) |
150 PDFLATEX=$(type -path pdflatex) |
151 |
151 |
152 for DOC in $(cat Contents) |
152 for DOC in $(cat Dirs) |
153 do |
153 do |
154 pushd "$DOC" > /dev/null |
154 pushd "$DOC" > /dev/null |
155 make dvi || fail "DVI document for $DOC failed!" |
155 make dvi || fail "DVI document for $DOC failed!" |
156 { [ -n "$PDFLATEX" ] && make clean pdf; } || fail "PDF document for $DOC failed!" |
156 { [ -n "$PDFLATEX" ] && make clean pdf; } || fail "PDF document for $DOC failed!" |
157 popd |
157 popd |