| changeset 27446 | bac210482607 |
| parent 27090 | 2f45c1b1b05d |
| child 27633 | c2984f0684ee |
--- a/Admin/makedist Wed Jul 02 19:52:57 2008 +0200 +++ b/Admin/makedist Wed Jul 02 20:13:32 2008 +0200 @@ -149,7 +149,7 @@ cd "$DISTBASE/$DISTNAME/Doc" PDFLATEX=$(type -path pdflatex) -for DOC in $(cat Contents) +for DOC in $(cat Dirs) do pushd "$DOC" > /dev/null make dvi || fail "DVI document for $DOC failed!"