diff -r 9ed940a1bebb -r 3057990d20e0 lib/Tools/latex
--- 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
 }