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/\$Id$]*)\$/originating from CVS: $1/g; print;' $STYLEFILE > $TARGET |
90 "$AUTO_PERL" -n -e 's/\$[I]d:?(?:\s)*([^\$]*)\$/originating from CVS: $1/g; print;' $STYLEFILE > $TARGET |
91 done |
91 done |
92 } |
92 } |
93 |
93 |
94 function extract_syms () |
94 function extract_syms () |
95 { |
95 { |