lib/Tools/usedir
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