1.1 --- a/lib/Tools/latex	Fri Mar 24 11:52:19 2000 +0100
     1.2 +++ b/lib/Tools/latex	Fri Mar 24 13:47:36 2000 +0100
     1.3 @@ -84,10 +84,10 @@
     1.4  {
     1.5    for NAME in $ISABELLE_HOME/lib/texinputs/*.sty
     1.6    do
     1.7 -    BNAME=$(basename "$NAME")
     1.8 -    if [ ! -e "$BNAME" -o "$NAME" -nt "$BNAME" ]; then
     1.9 -      echo "updating $BNAME"
    1.10 -      cp -f "$NAME" "$BNAME"
    1.11 +    DEST="$DIR"/$(basename "$NAME")
    1.12 +    if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then
    1.13 +      echo "updating $DEST"
    1.14 +      cp -f "$NAME" "$DEST"
    1.15      fi
    1.16    done
    1.17  }

     2.1 --- a/lib/Tools/usedir	Fri Mar 24 11:52:19 2000 +0100
     2.2 +++ b/lib/Tools/usedir	Fri Mar 24 13:47:36 2000 +0100
     2.3 @@ -135,6 +135,7 @@
     2.4  
     2.5  DOC=""
     2.6  [ "$DOCUMENT" != false -a -d document ] && DOC="$DOCUMENT"
     2.7 +[ -n "$DUMP" ] && $ISATOOL latex -o sty "$DUMP/root.tex" >/dev/null
     2.8  
     2.9  
    2.10  SECONDS=0