--- 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
}
--- 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