equal
deleted
inserted
replaced
198 # cleanup dist |
198 # cleanup dist |
199 |
199 |
200 mv "$DISTNAME" "${DISTNAME}-old" |
200 mv "$DISTNAME" "${DISTNAME}-old" |
201 mkdir "$DISTNAME" |
201 mkdir "$DISTNAME" |
202 |
202 |
203 mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \ |
203 mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \ |
204 "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \ |
204 "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME" |
205 "$DISTNAME" |
|
206 mkdir "$DISTNAME/doc" |
205 mkdir "$DISTNAME/doc" |
207 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" |
206 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" |
208 |
207 |
209 chgrp -R isabelle "$DISTNAME" |
208 chgrp -R isabelle "$DISTNAME" |
210 |
209 |