--- 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 ()