equal
deleted
inserted
replaced
215 chmod -R u+w "$DISTNAME" |
215 chmod -R u+w "$DISTNAME" |
216 chmod -R g=o "$DISTNAME" |
216 chmod -R g=o "$DISTNAME" |
217 chgrp -R isabelle "$DISTNAME" Isabelle |
217 chgrp -R isabelle "$DISTNAME" Isabelle |
218 |
218 |
219 mkdir -p "pdf/$DISTNAME/doc" |
219 mkdir -p "pdf/$DISTNAME/doc" |
220 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" |
220 mv "$DISTNAME/doc/"*.pdf "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc" |
221 |
221 |
222 echo "$DISTNAME.tar.gz" |
222 echo "$DISTNAME.tar.gz" |
223 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME" |
223 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME" |
224 gzip "$DISTNAME.tar" |
224 gzip "$DISTNAME.tar" |
225 |
225 |