# HG changeset patch
# User wenzelm
# Date 953902056 -3600
# Node ID 3c3895e377617c4dd3860961f33f2d9a183be28c
# Parent  37a1e855390ad6ed44996c6481862f15c47b190d
improved dump of styles;

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
 }
diff -r 37a1e855390a -r 3c3895e37761 lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Mar 24 11:52:19 2000 +0100
+++ b/lib/Tools/usedir	Fri Mar 24 13:47:36 2000 +0100
@@ -135,6 +135,7 @@
 
 DOC=""
 [ "$DOCUMENT" != false -a -d document ] && DOC="$DOCUMENT"
+[ -n "$DUMP" ] && $ISATOOL latex -o sty "$DUMP/root.tex" >/dev/null
 
 
 SECONDS=0