equal
deleted
inserted
replaced
82 |
82 |
83 function update_styles () |
83 function update_styles () |
84 { |
84 { |
85 for NAME in $ISABELLE_HOME/lib/texinputs/*.sty |
85 for NAME in $ISABELLE_HOME/lib/texinputs/*.sty |
86 do |
86 do |
87 BNAME=$(basename "$NAME") |
87 DEST="$DIR"/$(basename "$NAME") |
88 if [ ! -e "$BNAME" -o "$NAME" -nt "$BNAME" ]; then |
88 if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then |
89 echo "updating $BNAME" |
89 echo "updating $DEST" |
90 cp -f "$NAME" "$BNAME" |
90 cp -f "$NAME" "$DEST" |
91 fi |
91 fi |
92 done |
92 done |
93 } |
93 } |
94 |
94 |
95 case "$OUTFORMAT" in |
95 case "$OUTFORMAT" in |