changeset 8565 | 3c3895e37761 |
parent 8564 | 37a1e855390a |
child 8568 | b18540435f26 |
--- a/lib/Tools/latex Fri Mar 24 11:52:19 2000 +0100 +++ b/lib/Tools/latex Fri Mar 24 13:47:36 2000 +0100 @@ -84,10 +84,10 @@ { for NAME in $ISABELLE_HOME/lib/texinputs/*.sty do - BNAME=$(basename "$NAME") - if [ ! -e "$BNAME" -o "$NAME" -nt "$BNAME" ]; then - echo "updating $BNAME" - cp -f "$NAME" "$BNAME" + DEST="$DIR"/$(basename "$NAME") + if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then + echo "updating $DEST" + cp -f "$NAME" "$DEST" fi done }