equal
deleted
inserted
replaced
140 |
140 |
141 # create archive |
141 # create archive |
142 |
142 |
143 cd $DISTBASE |
143 cd $DISTBASE |
144 |
144 |
145 chown -R $LOGNAME:isabelle $DISTNAME |
145 #FIXME doesn't work!? |
146 chmod -R u+w $DISTNAME |
146 #chown -R $LOGNAME:isabelle $DISTNAME |
147 chmod -R g-w $DISTNAME |
147 #chmod -R u+w $DISTNAME |
|
148 #chmod -R g-w $DISTNAME |
148 |
149 |
149 tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz |
150 tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz |
150 |
151 |
151 |
152 |
152 # final note |
153 # final note |