equal
deleted
inserted
replaced
85 { |
85 { |
86 for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty |
86 for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty |
87 do |
87 do |
88 TARGET="$DIR"/$(basename $STYLEFILE) |
88 TARGET="$DIR"/$(basename $STYLEFILE) |
89 rm -f $TARGET |
89 rm -f $TARGET |
90 "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$/originating from CVS: $1/g; print;' $STYLEFILE > $TARGET |
90 "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$//g; print;' "$STYLEFILE" > "$TARGET" |
91 # the [I] is there to prevent CVS from expanding $Id...$ itself ;-) |
91 #~ "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$/originating from CVS: $1/g; print;' $STYLEFILE > $TARGET |
|
92 #~ # the [I] is there to prevent CVS from expanding $Id...$ itself ;-) |
92 done |
93 done |
93 } |
94 } |
94 |
95 |
95 function extract_syms () |
96 function extract_syms () |
96 { |
97 { |