# HG changeset patch # User haftmann # Date 1117609018 -7200 # Node ID 519d717ae9e375f7f7f8615c9527b83ead18ba98 # Parent 833f4160130ee928f07a00eae9bc420834315aff improved *.sty handling diff -r 833f4160130e -r 519d717ae9e3 lib/Tools/latex --- a/lib/Tools/latex Wed Jun 01 08:44:25 2005 +0200 +++ b/lib/Tools/latex Wed Jun 01 08:56:58 2005 +0200 @@ -83,8 +83,12 @@ function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } function copy_styles () { - cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; - "$AUTO_PERL" -n -i -e 's/\$Id(?::\s)*([^\$]*)\$/originating from CVS: $1/g; print;' "$DIR"/*.sty + for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty + do + TARGET="$DIR"/$(basename $STYLEFILE) + rm -f $TARGET + "$AUTO_PERL" -n -e 's/\$Id$]*)\$/originating from CVS: $1/g; print;' $STYLEFILE > $TARGET + done } function extract_syms ()