diff -r 37a1e855390a -r 3c3895e37761 lib/Tools/latex
--- 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
 }