--- a/lib/Tools/latex Tue Jul 19 16:16:53 2005 +0200
+++ b/lib/Tools/latex Tue Jul 19 17:21:45 2005 +0200
@@ -85,11 +85,8 @@
{
for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
do
- TARGET="$DIR"/$(basename $STYLEFILE)
- rm -f $TARGET
- "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g; print;' "$STYLEFILE" > "$TARGET"
- #~ "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$/originating from CVS: $1/g; print;' $STYLEFILE > $TARGET
- # the [I] is there to prevent CVS from expanding $Id...$ itself ;-)
+ TARGET="$DIR"/$(basename "$STYLEFILE")
+ "$AUTO_PERL" -p -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g' "$STYLEFILE" > "$TARGET"
done
}