tuned;
authorwenzelm
Fri, 24 Mar 2000 14:40:51 +0100
changeset 8568b18540435f26
parent 8567 e6d46b03f2cb
child 8569 748a9699f28d
tuned;
lib/Tools/latex
lib/Tools/usedir
     1.1 --- a/lib/Tools/latex	Fri Mar 24 13:48:31 2000 +0100
     1.2 +++ b/lib/Tools/latex	Fri Mar 24 14:40:51 2000 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4    FILEBASE=$DIR/$(basename "$FILE" .tex)
     1.5  fi
     1.6  
     1.7 -function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'" }
     1.8 +function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
     1.9  
    1.10  
    1.11  # operations
     2.1 --- a/lib/Tools/usedir	Fri Mar 24 13:48:31 2000 +0100
     2.2 +++ b/lib/Tools/usedir	Fri Mar 24 14:40:51 2000 +0100
     2.3 @@ -133,9 +133,12 @@
     2.4  
     2.5  [ -z "$BUILD" ] && cd "$NAME"
     2.6  
     2.7 -DOC=""
     2.8 -[ "$DOCUMENT" != false -a -d document ] && DOC="$DOCUMENT"
     2.9 -[ -n "$DUMP" ] && $ISATOOL latex -o sty "$DUMP/root.tex" >/dev/null
    2.10 +if [ "$DOCUMENT" != false -a -d document ]; then
    2.11 +  DOC="$DOCUMENT"
    2.12 +  [ -n "$DUMP" -a -d "$DUMP" ] && $ISATOOL latex -o sty "$DUMP/root.tex" >/dev/null
    2.13 +else
    2.14 +  DOC=""
    2.15 +fi
    2.16  
    2.17  
    2.18  SECONDS=0