changeset 8568 | b18540435f26 |
parent 8565 | 3c3895e37761 |
child 8747 | 22580c8bc62f |
--- a/lib/Tools/usedir Fri Mar 24 13:48:31 2000 +0100 +++ b/lib/Tools/usedir Fri Mar 24 14:40:51 2000 +0100 @@ -133,9 +133,12 @@ [ -z "$BUILD" ] && cd "$NAME" -DOC="" -[ "$DOCUMENT" != false -a -d document ] && DOC="$DOCUMENT" -[ -n "$DUMP" ] && $ISATOOL latex -o sty "$DUMP/root.tex" >/dev/null +if [ "$DOCUMENT" != false -a -d document ]; then + DOC="$DOCUMENT" + [ -n "$DUMP" -a -d "$DUMP" ] && $ISATOOL latex -o sty "$DUMP/root.tex" >/dev/null +else + DOC="" +fi SECONDS=0