equal
deleted
inserted
replaced
219 # cleanup dist |
219 # cleanup dist |
220 |
220 |
221 mv "$DISTNAME" "${DISTNAME}-old" |
221 mv "$DISTNAME" "${DISTNAME}-old" |
222 mkdir "$DISTNAME" |
222 mkdir "$DISTNAME" |
223 |
223 |
224 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "$DISTNAME" |
224 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" "$DISTNAME" |
225 mkdir "$DISTNAME/doc" |
225 mkdir "$DISTNAME/doc" |
226 mv "${DISTNAME}-old/doc/"*.pdf "$DISTNAME/doc" |
226 mv "${DISTNAME}-old/doc/"*.pdf "$DISTNAME/doc" |
227 |
227 |
228 chgrp -R isabelle "$DISTNAME" |
228 chgrp -R isabelle "$DISTNAME" |
229 |
229 |